---

Step * of Lemma rng_times_nat_op

∀[r:Rng]. ∀[a,b:|r|]. ∀[n:ℕ].  ((a * (n ⋅r b)) = (n ⋅r (a * b)) ∈ |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 : ℕ
⊢ (a * (Σ(r) 0 ≤ i < n. b)) = (Σ(r) 0 ≤ i < n. a * b) ∈ |r|

---

Latex:

---

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


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