Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-27 17:20 40e514cb

View on Github →

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

Estimated changes

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.lift_nc_smul

added theorem monoid_algebra.lift_nc_smul

modified theorem monoid_algebra.single_algebra_map_eq_algebra_map_mul_of