Def MulHom.piMap

Modification history

2026-06-04 11:07
Mathlib/Algebra/Group/Pi/Lemmas.lean
feat: define MonoidHom.piMap (#40032)
Added MulHom.piMapView on Github →