Commit 2025-11-28 16:39 6ccffb61

View on Github →

chore(to_additive): remove redundant entries from abbreviationDict (#32092) This PR removes some entries from the to_additive abbreviationDict. These were only used in noncommProd_mul_single which I have renamed to noncommProd_mulSingle.

Estimated changes

Modified Mathlib/Data/Finset/NoncommProd.lean

added theorem Finset.noncommProd_mulSingle

deleted theorem Finset.noncommProd_mul_single

Modified Mathlib/GroupTheory/Finiteness.lean

Modified Mathlib/Tactic/Translate/ToAdditive.lean

Modified MathlibTest/toAdditive.lean