Commit 2026-09-18 15:04 4e8414e2

View on Github →

chore: catch up on a lot of to_additive debt (#43814) This PR removes many uses of to_additive existing. Many of these used to be necessary, but are now not anymore thanks to various improvements to to_additive.

Estimated changes

deleted theorem Pi.single_induction
deleted theorem AddAction.toPerm_zero
deleted def SubNegMonoid.sub'
deleted theorem negSucc_zsmul
deleted def zsmulRec
modified theorem Finset.coe_prod
modified theorem Finset.prod_inv_index
modified theorem Finset.prod_neg_index
deleted theorem Finset.sum_inv_index
deleted def WithZero.recZeroCoe
deleted theorem SymAlg.sym_neg
deleted theorem SymAlg.unsym_neg
deleted theorem AddGroupNorm.apply_one
deleted theorem AddGroupSeminorm.smul_sup
deleted theorem FunLike.coe_smul
deleted theorem LocallyConstant.coe_smul