---

Step * of Lemma rng_times_over_plus

∀[r:Rng]. ∀[a,b,c:|r|].  (((a * (b +r c)) = ((a * b) +r (a * c)) ∈ |r|) ∧ (((b +r c) * a) = ((b * a) +r (c * a)) ∈ |r|))
BY
{ Fold `bilinear` 0 
THEN ((D 0) THENA Auto) }

1
1. r : Rng
⊢ BiLinear(|r|;+r;*)

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b,c:|r|].
    (((a  *  (b  +r  c))  =  ((a  *  b)  +r  (a  *  c)))  \mwedge{}  (((b  +r  c)  *  a)  =  ((b  *  a)  +r  (c  *  a))))


By

---

Latex:
Fold  `bilinear`  0 
THEN  ((D  0)  THENA  Auto)

---

Home Index