Commit 2026-07-13 18:36 8ccb2141

View on Github →

chore: use to_additive in more places (#29145) This PR addresses some comments about to_additive not working, by making it work more.

Estimated changes

Modified Mathlib/Combinatorics/Additive/DoublingConst.lean

deleted theorem Finset.card_mul_cast_addConst

deleted theorem Finset.card_mul_cast_subConst

deleted theorem Finset.cast_addConst

deleted theorem Finset.cast_addConst_mul_card

deleted theorem Finset.cast_subConst

deleted theorem Finset.cast_subConst_mul_card

Modified Mathlib/Topology/Algebra/InfiniteSum/Module.lean

deleted theorem AddAction.automorphize_smul_left