Commit 2025-09-03 02:00 315dd708

View on Github →

style: HasContinuousInv₀ to ContinuousInv₀ (#29201) ContinuousAdd, ContinuousNeg, ContinuousInv but HasContinuousInv₀, this is inconsistent.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

added theorem continuousInv₀_of_contMDiffInv₀

deleted theorem hasContinuousInv₀_of_hasContMDiffInv₀

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/Topology/Algebra/Field.lean

modified theorem IsPreconnected.eq_of_sq_eq

modified theorem IsPreconnected.eq_or_eq_neg_of_sq_eq

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

added theorem ContinuousInv₀.of_nhds_one

deleted theorem HasContinuousInv₀.of_nhds_one

Modified Mathlib/Topology/Algebra/IsOpenUnits.lean

Modified Mathlib/Topology/Algebra/Order/Field.lean

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

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

Modified Mathlib/Topology/Instances/Rat.lean