---

Step * of Lemma princ_ideal_wf

∀[r:Rng]. ∀[a:|r|].  ((a)r ∈ Ideal(r){i})
BY
{ Auto }

1
1. r : Rng
2. a : |r|
⊢ (a)r ∈ Ideal(r){i}

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a:|r|].    ((a)r  \mmember{}  Ideal(r)\{i\})


By

---

Latex:
Auto

---

Home Index