Commit 2026-02-15 11:14 946b120a

View on Github →

feat(to_additive): automatically infer relevant_arg (#35318) This PR implements a better heuristic in to_additive for figuring out the (relevant_arg := ...) option. After this PR, there is only one place where the option needs to be provided manually: the definition of MonoidAlgebra. A future PR may do a similar change, but for the dont_translate option.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Limits.lean

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Modified Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

Modified Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean

Modified Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean

Modified Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean

Modified Mathlib/Tactic/Translate/Core.lean

added inductive Mathlib.Tactic.Translate.RelevantArg

added def Mathlib.Tactic.Translate.ReplacementM.run

deleted def Mathlib.Tactic.Translate.changeNumeral

deleted def Mathlib.Tactic.Translate.findRelevantArg

modified def Mathlib.Tactic.Translate.findTargetName

added def Mathlib.Tactic.Translate.getRelevantArg

modified def Mathlib.Tactic.Translate.proceedFields

modified def Mathlib.Tactic.Translate.proceedFieldsAux

deleted def Mathlib.Tactic.Translate.shouldTranslate

Modified Mathlib/Tactic/Translate/TagUnfoldBoundary.lean

Modified MathlibTest/toAdditive.lean

deleted structure AddMonoidAlgebra'

added structure AddMonoidAlgebra

deleted structure MonoidAlgebra'

added structure MonoidAlgebra

added def monoidAlgebraFoo

added def monoidAlgebraFoo₁

added def monoidAlgebraFoo₂