Theorem MulHom.pi_injective

Modification history

2026-06-04 11:07

Mathlib/Algebra/Group/Pi/Lemmas.lean

feat: define MonoidHom.piMap (#40032)

Modified MulHom.pi_injective View on Github →

2026-05-30 13:01

Mathlib/Algebra/Group/Pi/Lemmas.lean

chore: rename MonoidHom.injective_pi to pi_injective (#40045) …

Added MulHom.pi_injective View on Github →