Commit 2023-04-26 12:39 a5ac4ef3

View on Github →

chore: forward-port leanprover-community/mathlib#18852 (#3646) This additionally makes a further small generalization to some of the finsupp instances (labelled with porting notes) which should be backported. The new statement of Rat.smul_one_eq_coe fixes a proof in Mathlib/Analysis/NormedSpace/Basic.lean that was mangled during porting.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

deleted theorem Rat.smul_one_eq_coe

Modified Mathlib/Algebra/Field/Defs.lean

added theorem Rat.smul_one_eq_coe

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.coe_smul

modified theorem Finsupp.smul_apply

modified theorem Finsupp.smul_single

modified theorem IsSMulRegular.finsupp

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.rat_smul_eq_C_mul

modified theorem Polynomial.smul_C

modified theorem Polynomial.smul_monomial

Modified Mathlib/Data/Polynomial/Coeff.lean

modified theorem Polynomial.coeff_smul