Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 18:09 7a37dd4e

View on Github →

feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into a ring_hom and alg_hom (#4789)

Estimated changes

Modified src/algebra/monoid_algebra.lean

added def add_monoid_algebra.lift_nc_alg_hom

added def add_monoid_algebra.lift_nc_ring_hom

added def monoid_algebra.lift_nc_alg_hom

added def monoid_algebra.lift_nc_ring_hom