Commit 2025-08-01 21:30 968ea7f2

View on Github →

chore: tidy various files (#27630)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

modified theorem AlgebraicGeometry.AffineSpace.spec_le_iff

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Data/Matrix/Diagonal.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

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

Modified Mathlib/GroupTheory/Abelianization/Defs.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/Basic.lean

Modified Mathlib/Probability/Moments/Covariance.lean

modified theorem ProbabilityTheory.covariance_mul_left

modified theorem ProbabilityTheory.covariance_mul_right

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

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/Order/HullKernel.lean