Commit 2024-10-27 10:54 1eb2db95

View on Github →

fix(Algebra/MonoidAlgebra/Basic): resolve ext porting notes (#6524)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

added theorem AddMonoidAlgebra.addHom_ext'

added theorem AddMonoidAlgebra.distribMulActionHom_ext'

added theorem AddMonoidAlgebra.ext

added theorem AddMonoidAlgebra.lhom_ext'

added theorem AddMonoidAlgebra.lsingle_apply

added theorem AddMonoidAlgebra.singleAddHom_apply

added theorem MonoidAlgebra.addHom_ext'

added theorem MonoidAlgebra.distribMulActionHom_ext'

added theorem MonoidAlgebra.ext

added theorem MonoidAlgebra.lhom_ext'

added theorem MonoidAlgebra.lsingle_apply

added theorem MonoidAlgebra.singleAddHom_apply

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean