Commit 2025-07-16 20:44 f2ef6e56

View on Github →

chore: tidy various files (#27220)

Estimated changes

Modified Archive/Imo/Imo2024Q3.lean

Modified Mathlib/Algebra/CharP/Defs.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Range.lean

modified theorem MonoidWithZeroHom.coe_one

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/Analysis/Calculus/DerivativeTest.lean

Modified Mathlib/Analysis/Calculus/VectorField.lean

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean

Modified Mathlib/Data/Finsupp/Option.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/Nat/Digits/Defs.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

Modified Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

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

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

Modified Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

Modified Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Modified Mathlib/RingTheory/Valuation/Discrete/Basic.lean

modified theorem Valuation.IsRankOneDiscrete.generator_lt_one

modified theorem Valuation.IsRankOneDiscrete.generator_ne_one

Modified Mathlib/RingTheory/Valuation/ValuativeRel.lean

Modified Mathlib/RingTheory/ZMod/UnitsCyclic.lean

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

Modified Mathlib/Topology/ShrinkingLemma.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean