Commit 2025-08-06 09:16 1e4b2ade

View on Github →

chore(Algebra/Group/Support): rename primed lemmas to match naming convention (#27777) mulSupport_inv should be called mulSupport_fun_inv, according to the naming convention, similarly for the other lemmas. Unfortunately, there is no good tooling yet for renames A -> B and B -> C.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/Group/Indicator.lean

Modified Mathlib/Algebra/Group/Support.lean

deleted theorem Function.mulSupport_curry'

added theorem Function.mulSupport_fun_curry

added theorem Function.mulSupport_fun_inv

added theorem Function.mulSupport_fun_one

deleted theorem Function.mulSupport_inv'

modified theorem Function.mulSupport_inv

deleted theorem Function.mulSupport_one'

modified theorem Function.mulSupport_one

added theorem Function.mulSupport_prodMk'

added theorem Function.mulSupport_prodMk

deleted theorem Function.mulSupport_prod_mk'

deleted theorem Function.mulSupport_prod_mk

Modified Mathlib/Algebra/GroupWithZero/Indicator.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/Topology/Algebra/Support.lean

Modified Mathlib/Topology/LocallyFinsupp.lean