Mathlib v3 is deprecated. Go to Mathlib v4

Def add_monoid_algebra.lift_nc_ring_hom

Modification history

2020-10-28 18:09
src/algebra/monoid_algebra.lean
feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into a ring_hom and alg_hom (#4789)
Added add_monoid_algebra.lift_nc_ring_homView on Github →