---

Step * of Lemma ideal-detach-equiv

∀r:CRng. ∀a:Ideal(r){i}.  ((∀x:|r|. SqStable(a x)) ⇒ (∀d:detach_fun(|r|;a). EquivRel(|r|;x,y.↑(d (x +r (-r y))))))
BY
{ EAuto 1 }

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}a:Ideal(r)\{i\}.
    ((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  (\mforall{}d:detach\_fun(|r|;a).  EquivRel(|r|;x,y.\muparrow{}(d  (x  +r  (-r  y))))))


By

---

Latex:
EAuto  1

---

Home Index