mathlib

a2f3f55e - chore(algebra/monoid_algebra): generalize lift_nc (#11881)

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