---

Step * of Lemma rng_times_nat_op_r

∀[r:Rng]. ∀[a,b:|r|]. ∀[n:ℕ].  (((n ⋅r b) * a) = (n ⋅r (b * a)) ∈ |r|)
BY
{ ((UnivCD) THENA Auto) 
THEN RepUnfolds ``rng_nat_op mon_nat_op nat_op`` 0 
THEN Repeat (Folds ``mon_itop rng_sum`` 0) 
 }

1
1. r : Rng
2. a : |r|
3. b : |r|
4. n : ℕ
⊢ ((Σ(r) 0 ≤ i < n. b) * a) = (Σ(r) 0 ≤ i < n. b * a) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].  \mforall{}[n:\mBbbN{}].    (((n  \mcdot{}r  b)  *  a)  =  (n  \mcdot{}r  (b  *  a)))


By

---

Latex:
((UnivCD)  THENA  Auto) 
THEN  RepUnfolds  ``rng\_nat\_op  mon\_nat\_op  nat\_op``  0 
THEN  Repeat  (Folds  ``mon\_itop  rng\_sum``  0) 

---

Home Index