Commit 2026-03-16 05:13 f4a09007

View on Github →

feat(translate): support to_additive (attr := to_fun) (#36305) This PR adds extensible support for letting to_additive/to_dual interact with other attributes that create declarations, such as to_fun and simps. Previously, this behaviour was hard-coded just for simps. This PR removes simps from the imports of Translate.Core. For this, simps is removed from the existing attribute linter.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/FiniteSupport/Basic.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Notation/Defs.lean

Modified Mathlib/Lean/Meta/Simp.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

modified theorem AEMeasurable.const_smul

deleted theorem AEMeasurable.fun_const_smul

deleted theorem Measurable.fun_const_smul

Modified Mathlib/Order/Defs/LinearOrder.lean

Modified Mathlib/Order/Defs/Unbundled.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.EventuallyEq.fun_div

deleted theorem Filter.EventuallyEq.fun_inv

deleted theorem Filter.EventuallyEq.fun_mul

deleted theorem Filter.EventuallyEq.fun_pow_const

Modified Mathlib/Order/Notation.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/ToFun.lean

added def Mathlib.Tactic.toFunImpl

Created Mathlib/Tactic/Translate/Attributes.lean

added def Mathlib.Tactic.registerGeneratingAttr

Modified Mathlib/Tactic/Translate/Core.lean

Modified Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean