Step
*
of Lemma
nat_int_grp_sig_hom
IsMonHomInj(<ℕ,+><ℤ+>λx.x)
BY
{ ((AGenRepD ["basic";"compound"] 
THEN OnAllClauses Reduce ) THEN Auto) }
Latex:
Latex:
IsMonHomInj(<\mBbbN{},+><\mBbbZ{}+>\mlambda{}x.x)
By
Latex:
((AGenRepD  ["basic";"compound"] 
THEN  OnAllClauses  Reduce  )  THEN  Auto)
Home
Index