Commit 2026-06-04 11:07 439e0024

View on Github →

feat: define MonoidHom.piMap (#40032)

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

modified def MonoidHom.pi

added def MonoidHom.piMap

modified theorem MonoidHom.pi_injective

modified def MulHom.pi

added def MulHom.piMap

modified theorem MulHom.pi_injective