Commit 2026-03-26 16:39 2f18538b

View on Github →

chore(MonoidAlgebra): clean up instances (#37213) Clean up the instances on MonoidAlgebra using inferInstanceAs

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

modified theorem MonoidAlgebra.single_add

modified theorem MonoidAlgebra.single_neg

modified theorem MonoidAlgebra.single_zero

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean