Commit 2026-05-30 08:25 72a04447

View on Github →

chore: rename Pi.monoidHom to MonoidHom.pi (#40024) Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Pi.2EfooHom.20or.20FooHom.2Epi/near/598538630

Estimated changes

added theorem MonoidHom.injective_pi
added def MonoidHom.pi
added theorem MulHom.injective_pi
added def MulHom.pi
deleted def Pi.monoidHom
deleted theorem Pi.monoidHom_injective
deleted def Pi.mulHom
deleted theorem Pi.mulHom_injective