Commit 2025-07-22 22:48 f41e2155

View on Github →

feat(MonoidAlgebra): miscellaneous basic lemmas (#27199) From Toric

Estimated changes

Modified Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

added theorem AddMonoidAlgebra.coe_add

added theorem AddMonoidAlgebra.liftNCRingHom_single

added theorem AddMonoidAlgebra.neg_apply

added theorem AddMonoidAlgebra.single_neg

added theorem AddMonoidAlgebra.smul_apply

added theorem MonoidAlgebra.coe_add

added theorem MonoidAlgebra.induction_linear

added theorem MonoidAlgebra.liftNCRingHom_single

added theorem MonoidAlgebra.neg_apply

added theorem MonoidAlgebra.single_neg

added theorem MonoidAlgebra.smul_apply

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified scripts/nolints.json