---

Step * of Lemma sq_stable__ideal_p

∀r:CRng. ∀a:|r| ⟶ ℙ.  ((∀x:|r|. SqStable(a x)) ⇒ SqStable(a Ideal of r))
BY
{ (Unfold `ideal_p` 0 THEN Auto THEN Unfold `subgrp_p` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}a:|r|  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  SqStable(a  Ideal  of  r))


By

---

Latex:
(Unfold  `ideal\_p`  0  THEN  Auto  THEN  Unfold  `subgrp\_p`  0  THEN  Auto)

---

Home Index