Commit 2022-02-07 14:32 a2f3f55e

View on Github →

chore(algebra/monoid_algebra): generalize lift_nc (#11881) The g argument does not need to be a bundled morphism here in the definition. Instead, we require it be a bundled morphism only in the downstream lemmas, using the new typeclass machinery

Estimated changes

Modified src/algebra/monoid_algebra/basic.lean

modified def add_monoid_algebra.lift_nc

modified theorem add_monoid_algebra.lift_nc_mul

modified theorem add_monoid_algebra.lift_nc_one

modified theorem add_monoid_algebra.lift_nc_single

modified def monoid_algebra.lift_nc

modified theorem monoid_algebra.lift_nc_mul

modified theorem monoid_algebra.lift_nc_one

modified theorem monoid_algebra.lift_nc_single