Mathlib v3 is deprecated. Go to Mathlib v4

Def pi.const_monoid_hom

Modification history

2021-08-10 09:12
src/algebra/group/pi.lean
feat(algebra/group/pi): Add `pi.const_(monoid|add_monoid|ring|alg)_hom` (#8518)
Added pi.const_monoid_homView on Github →