Step
*
of Lemma
abgrp_wf
AbGrp ∈ 𝕌'
BY
{ Unfold `abgrp` 0 THEN Auto }
Latex:
Latex:
AbGrp  \mmember{}  \mBbbU{}'
By
Latex:
Unfold  `abgrp`  0  THEN  Auto
Home
Index