Commit 2025-08-18 19:46 37e871dc

View on Github →

chore: tidy various files (#28461)

Estimated changes

Modified Archive/Imo/Imo1981Q3.lean

modified theorem Imo1981Q3.NatPredicate.imp_fib

Modified Archive/Imo/Imo2001Q4.lean

Modified Archive/Imo/Imo2021Q1.lean

Modified Mathlib/Algebra/Field/Equiv.lean

Modified Mathlib/Algebra/Group/TypeTags/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/Algebra/Order/Hom/TypeTags.lean

Modified Mathlib/Algebra/QuaternionBasis.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean

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

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

Modified Mathlib/Combinatorics/Quiver/Path.lean

Modified Mathlib/Combinatorics/Quiver/Path/Decomposition.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Insert.lean

Modified Mathlib/Data/Finset/Lattice/Lemmas.lean

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

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

Modified Mathlib/Probability/HasLaw.lean

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/InfinitePi.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/Probability/Process/FiniteDimensionalLaws.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

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

Modified Mathlib/Topology/Order/IntermediateValue.lean