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