Commit 2026-01-14 14:17 a0ec5d2c

View on Github →

feat(to_dual): linter for redundant uses of to_dual/to_additive (#33239) This PR adds a linter that helps avoid unneccessary uses of to_dual/to_additive. With to_dual self it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.

Estimated changes

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

modified theorem WithOne.«exists»

modified theorem WithOne.«forall»

Modified Mathlib/Analysis/Normed/Group/Continuity.lean

deleted theorem Filter.Tendsto.enorm'

added theorem Filter.Tendsto.enorm

deleted theorem Inseparable.enorm_eq_enorm'

added theorem Inseparable.enorm_eq_enorm

Modified Mathlib/CategoryTheory/Types/Basic.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Defs/PartialOrder.lean

modified theorem lt_irrefl

Modified Mathlib/Tactic/Translate/Core.lean

Modified Mathlib/Tactic/Translate/ToAdditive.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified MathlibTest/DeprecateTo.lean

Modified MathlibTest/Lint.lean

Modified MathlibTest/ToDual.lean

deleted theorem not_lt_self

Modified MathlibTest/toAdditive.lean