Mathlib v3 is deprecated. Go to Mathlib v4

Def pi.const_ring_hom

Modification history

2021-08-10 09:12

src/algebra/ring/pi.lean

feat(algebra/group/pi): Add `pi.const_(monoid|add_monoid|ring|alg)_hom` (#8518)

Added pi.const_ring_hom View on Github →