Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-02 20:41 76658a41

View on Github →

feat(algebra/group/pi): add pi.monoid_hom (#17757) Add the monoid version of pi.ring_hom.

Estimated changes

added def pi.monoid_hom
added def pi.mul_hom
added theorem pi.mul_hom_injective
modified def linear_map.pi