Commit 2023-04-24 13:09 2651125b

View on Github →

feat(algebra & polynomial): some (q)smul lemmas+generalisations (#18852) There is many generalisations around these areas too, but I am specifically not doing them as it will be easier done after the port. I am only doing what I need for merging in the splitting field diamond fix.

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem rat.smul_one_eq_coe

Modified src/algebra/field/defs.lean

added theorem rat.smul_one_eq_coe

Modified src/algebra/monoid_algebra/basic.lean

Modified src/data/finsupp/basic.lean

modified theorem finsupp.coe_smul

modified theorem finsupp.smul_apply

modified theorem finsupp.smul_single

modified theorem is_smul_regular.finsupp

Modified src/data/polynomial/basic.lean

added theorem polynomial.rat_smul_eq_C_mul

modified theorem polynomial.smul_C

modified theorem polynomial.smul_monomial

Modified src/data/polynomial/coeff.lean

modified theorem polynomial.coeff_smul