Commit 2026-10-28 08:06 435530e2

View on Github →

chore: decapitalize TFAE in theorem names (#45348) According to the naming convention, TFAE needs to be decapitalized in theorem names. This PR ensures this rule is followed in mathlib.

Estimated changes

Modified Mathlib/Algebra/Category/Ring/FilteredColimitsLocal.lean

Modified Mathlib/Algebra/Group/Units/Hom.lean

Modified Mathlib/Analysis/Analytic/ConvergenceRadius.lean

Modified Mathlib/Analysis/Analytic/RadiusLiminf.lean

Modified Mathlib/Analysis/BoxIntegral/Box/Basic.lean

deleted theorem BoxIntegral.Box.le_TFAE

added theorem BoxIntegral.Box.le_tfae

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

deleted theorem RCLike.is_real_TFAE

added theorem RCLike.is_real_tfae

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

deleted theorem CStarAlgebra.isStrictlyPositive_TFAE

added theorem CStarAlgebra.isStrictlyPositive_tfae

deleted theorem CStarAlgebra.nonneg_TFAE

added theorem CStarAlgebra.nonneg_tfae

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

deleted theorem TFAE_exists_lt_isLittleO_pow

added theorem tfae_exists_lt_isLittleO_pow

Modified Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

deleted theorem CategoryTheory.Bicategory.isLeftAdjoint_TFAE

added theorem CategoryTheory.Bicategory.isLeftAdjoint_tfae

deleted theorem CategoryTheory.Bicategory.isRightAdjoint_TFAE

added theorem CategoryTheory.Bicategory.isRightAdjoint_tfae

Modified Mathlib/RingTheory/AdicCompletion/LocalRing.lean

Modified Mathlib/RingTheory/Bezout.lean

deleted theorem IsBezout.TFAE

added theorem IsBezout.tfae

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

deleted theorem IsLocalRing.local_hom_TFAE

added theorem IsLocalRing.local_hom_tfae

Modified Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/Unramified/LocalRing.lean

Modified Mathlib/RingTheory/Valuation/Archimedean.lean

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

added theorem ValuationRing.tfae

Modified Mathlib/Topology/Inseparable.lean

deleted theorem specializes_TFAE

added theorem specializes_tfae

Modified Mathlib/Topology/NoetherianSpace.lean

deleted theorem TopologicalSpace.noetherianSpace_TFAE

added theorem TopologicalSpace.noetherianSpace_tfae

Modified Mathlib/Topology/Order/LeftRightNhds.lean

deleted theorem TFAE_mem_nhdsGE

deleted theorem TFAE_mem_nhdsGT

added theorem tfae_mem_nhdsGE

added theorem tfae_mem_nhdsGT

Modified Mathlib/Topology/Separation/Basic.lean

deleted theorem t1Space_TFAE

added theorem t1Space_tfae

Modified Mathlib/Topology/Separation/Connected.lean

Modified Mathlib/Topology/Separation/Regular.lean

deleted theorem regularSpace_TFAE

added theorem regularSpace_tfae

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

deleted theorem tendstoLocallyUniformlyOn_TFAE

added theorem tendstoLocallyUniformlyOn_tfae