Commit 2024-12-21 23:59 c459ca02

View on Github →

fix(to_additive): automatically translate all instances generated by extends (#19302) Fixes #660

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

Modified Mathlib/Algebra/Group/Hom/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Defs.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

modified def ToAdditive.proceedFieldsAux