---

Step * of Lemma mon_when_is_hom

∀[g:IMonoid]. ∀[b:𝔹].  IsMonHom{g,g}(λp:|g|. when b. p)
BY
{ ((AGenRepD ["basic";"compound"] 
THENM Reduce 0 
THENM Backchain ``mon_when_of_id mon_when_thru_op``) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[b:\mBbbB{}].    IsMonHom\{g,g\}(\mlambda{}p:|g|.  when  b.  p)


By

---

Latex:
((AGenRepD  ["basic";"compound"] 
THENM  Reduce  0 
THENM  Backchain  ``mon\_when\_of\_id  mon\_when\_thru\_op``)  THENA  Auto)

---

Home Index