feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)` (#4782)
feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)` (#4782)





leanprover-community/mathlib,leanprover-community/mathlib