Commit 2025-07-07 22:34 41615e95

View on Github →

chore: tidy various files (#26883)

Estimated changes

Modified Archive/Imo/Imo2001Q3.lean

Modified Archive/MiuLanguage/DecisionSuf.lean

Modified Archive/Sensitivity.lean

modified theorem Sensitivity.f_matrix

Modified Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Split.lean

Modified Mathlib/Analysis/RCLike/TangentCone.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/Combinatorics/Quiver/Path.lean

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Modified Mathlib/Data/Countable/Basic.lean

Modified Mathlib/Geometry/Euclidean/Altitude.lean

Modified Mathlib/Geometry/Euclidean/Incenter.lean

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

Modified Mathlib/ModelTheory/Satisfiability.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/Max.lean

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

modified theorem IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Submodule.smul_le_span

Modified Mathlib/RingTheory/Localization/AtPrime.lean

Modified Mathlib/RingTheory/OrderOfVanishing.lean

modified theorem Ring.ordFrac_eq_ord

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

Modified Mathlib/Topology/Connected/PathComponentOne.lean

Modified Mathlib/Topology/MetricSpace/HolderNorm.lean