Def MulHom.pi

Modification history

2026-06-04 11:07

Mathlib/Algebra/Group/Pi/Lemmas.lean

feat: define MonoidHom.piMap (#40032)

Modified MulHom.pi View on Github →

2026-05-30 08:25

Mathlib/Algebra/Group/Pi/Lemmas.lean

chore: rename Pi.monoidHom to MonoidHom.pi (#40024) …

Added MulHom.pi View on Github →