Commit 2025-10-14 00:50 1d032835

View on Github →

chore(MonoidAlgebra/Defs): reorder, rename variables (#29207) Sort the declarations according to typeclass assumptions, and according to the order in which we need them to be for #25273. Rename the semiring variable to R and the monoid one to M. Simultaneously golf. The rename is motivated by the idea that variables should reflect the generality, if such generality is used, and indeed such generality is definitely used since polynomials over a ring are the same thing as AddMonoidAlgebra R ℕ, and we neither have R a field nor ℕ a group. Furthermore, the file isn't entirely consistent with its use of variables to begin with, and that was causing me issues when resectioning.

Estimated changes

modified def AddMonoidAlgebra.of'
modified theorem AddMonoidAlgebra.of'_apply
modified theorem AddMonoidAlgebra.of'_eq_of
modified def AddMonoidAlgebra.of
modified theorem AddMonoidAlgebra.of_apply
modified theorem MonoidAlgebra.addHom_ext'
modified theorem MonoidAlgebra.ext
modified theorem MonoidAlgebra.induction_on
modified theorem MonoidAlgebra.intCast_def
modified def MonoidAlgebra.mul'
modified theorem MonoidAlgebra.mul_apply
modified theorem MonoidAlgebra.mul_def
modified theorem MonoidAlgebra.natCast_def
modified def MonoidAlgebra.of
modified def MonoidAlgebra.ofMagma
modified theorem MonoidAlgebra.of_commute
modified theorem MonoidAlgebra.of_injective
modified theorem MonoidAlgebra.one_def
modified theorem MonoidAlgebra.prod_single
modified theorem MonoidAlgebra.ringHom_ext'
modified theorem MonoidAlgebra.ringHom_ext
modified theorem MonoidAlgebra.single_add
modified theorem MonoidAlgebra.single_apply
modified theorem MonoidAlgebra.single_neg
modified theorem MonoidAlgebra.single_pow
modified theorem MonoidAlgebra.single_zero
modified theorem MonoidAlgebra.smul_apply
modified theorem MonoidAlgebra.smul_single
modified theorem MonoidAlgebra.sum_single
modified def MonoidAlgebra