Step * of Lemma mcomp_imp_not_unit

g:IAbMonoid. ∀a:|g|.  (Reducible(a)  (g-unit(a))))
BY
UnivCD THENA Auto }

1
1. IAbMonoid
2. |g|
3. Reducible(a)
⊢ ¬(g-unit(a))


Latex:


Latex:
\mforall{}g:IAbMonoid.  \mforall{}a:|g|.    (Reducible(a)  {}\mRightarrow{}  (\mneg{}(g-unit(a))))


By


Latex:
UnivCD  THENA  Auto




Home Index