---

Step * of Lemma int-to-ring-mul

∀[r:Rng]. ∀[a1,a2:ℤ].  (int-to-ring(r;a1 * a2) = (int-to-ring(r;a1) * int-to-ring(r;a2)) ∈ |r|)
BY
{ Auto }

1
1. r : Rng
2. a1 : ℤ
3. a2 : ℤ
⊢ int-to-ring(r;a1 * a2) = (int-to-ring(r;a1) * int-to-ring(r;a2)) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a1,a2:\mBbbZ{}].    (int-to-ring(r;a1  *  a2)  =  (int-to-ring(r;a1)  *  int-to-ring(r;a2)))


By

---

Latex:
Auto

---

Home Index