Commit 2026-03-04 08:58 bf8875c7

View on Github →

chore: adapt names after #34658 (#36080) This fixes the remaining theorem names referring to finite_{mulS|s}upport where the statement has changed to involve HasFinite{Mul}Support.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

deleted theorem finite_mulSupport_of_finprod_ne_one

deleted theorem finite_support_of_finsum_eq_one

added theorem hasFiniteMulSupport_of_finprod_ne_one

added theorem hasFiniteSupport_of_finsum_eq_one

Modified Mathlib/Algebra/DirectSum/Basic.lean

deleted theorem DirectSum.finite_support

added theorem DirectSum.hasFiniteSupport

Modified Mathlib/Algebra/FiniteSupport/Basic.lean

Modified Mathlib/Data/Finsupp/Defs.lean

deleted theorem Finsupp.finite_support

added theorem Finsupp.hasFiniteSupport

Modified Mathlib/Data/Finsupp/Pointwise.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/NumberTheory/Height/Basic.lean

Modified Mathlib/NumberTheory/Height/NumberField.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.hasFiniteMulSupport

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.hasFiniteMulSupport_int

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mulSupport_finite

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mulSupport_finite_int

Modified Mathlib/NumberTheory/NumberField/ProductFormula.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

deleted theorem Ideal.finite_mulSupport

deleted theorem Ideal.finite_mulSupport_coe

deleted theorem Ideal.finite_mulSupport_inv

added theorem Ideal.hasFiniteMulSupport

added theorem Ideal.hasFiniteMulSupport_coe

added theorem Ideal.hasFiniteMulSupport_inv

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

added theorem HahnSeries.SummableFamily.hasFiniteSupport_smul

deleted theorem HahnSeries.SummableFamily.smul_support_finite

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

deleted theorem Multipliable.finite_mulSupport_of_discreteTopology

added theorem Multipliable.hasFiniteMulSupport_of_discreteTopology

Modified Mathlib/Topology/Algebra/Ring/Compact.lean