Step * of Lemma grp_inverse

[g:IGroup]. ∀[a:|g|].  (((a (~ a)) e ∈ |g|) ∧ (((~ a) a) e ∈ |g|))
BY
Fold `inverse` THEN 
THENM THEN Auto }


Latex:


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


By


Latex:
Fold  `inverse`  0  THEN  D  0 
THENM  D  1  THEN  Auto




Home Index