Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-10 09:12 e8fc4663

View on Github →

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

Estimated changes

Modified src/algebra/algebra/basic.lean

added def pi.const_alg_hom

added theorem pi.const_alg_hom_eq_algebra_of_id

added theorem pi.const_ring_hom_eq_algebra_map

Modified src/algebra/group/pi.lean

added def pi.const_monoid_hom

Modified src/algebra/ring/pi.lean

added def pi.const_ring_hom

deleted theorem pi.ring_hom_apply

added theorem pi.ring_hom_injective