mathlib3

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