---

Step * of Lemma nat_op_mon_hom_2

∀[g:IAbMonoid]. ∀[n:ℕ].  IsMonHom{g,g}(λa.(n ⋅ a))
BY
{ ((Eval ``monoid_hom_p fun_thru_2op`` 0 
THENM Backchain ``mon_nat_op_id mon_nat_op_op``) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}[g:IAbMonoid].  \mforall{}[n:\mBbbN{}].    IsMonHom\{g,g\}(\mlambda{}a.(n  \mcdot{}  a))


By

---

Latex:
((Eval  ``monoid\_hom\_p  fun\_thru\_2op``  0 
THENM  Backchain  ``mon\_nat\_op\_id  mon\_nat\_op\_op``)  THENA  Auto)

---

Home Index