---

Step * 1 2 1 of Lemma mul-monomials-ringeq


1. r : CRng
2. v : |r|
3. v1 : |r|
4. v2 : |r|
5. v3 : |r|
⊢ ((v2 * v3) * (v * v1)) = ((v2 * v) * (v3 * v1)) ∈ |r|
BY
{ (RW CRngNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  v  :  |r|
3.  v1  :  |r|
4.  v2  :  |r|
5.  v3  :  |r|
\mvdash{}  ((v2  *  v3)  *  (v  *  v1))  =  ((v2  *  v)  *  (v3  *  v1))


By

---

Latex:
(RW  CRngNormC  0  THEN  Auto)

---

Home Index