Step
*
of Lemma
zero_ideal_wf
∀[r:CRng]. ((0r) ∈ Ideal(r){i})
BY
{ (Unfolds ``ideal zero_ideal`` 0 THEN Auto) }
1
1. r : CRng
⊢ λu.(u = 0 ∈ |r|) ∈ {p:|r| ⟶ ℙ| p Ideal of r}
Latex:
Latex:
\mforall{}[r:CRng]. ((0r) \mmember{} Ideal(r)\{i\})
By
Latex:
(Unfolds ``ideal zero\_ideal`` 0 THEN Auto)
Home
Index