---

Step * of Lemma grp_inv_diff

∀[g:IGroup]. ∀[a,b:|g|].  ((~ (a * (~ b))) = (b * (~ a)) ∈ |g|)
BY
{ ((RepD THENM RW GrpNormC 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:IGroup].  \mforall{}[a,b:|g|].    ((\msim{}  (a  *  (\msim{}  b)))  =  (b  *  (\msim{}  a)))


By

---

Latex:
((RepD  THENM  RW  GrpNormC  0)  THEN  Auto)

---

Home Index