Commit 2025-09-27 11:48 0b06a5db

View on Github →

chore: tidy various files (#29841)

Estimated changes

Modified Mathlib/Algebra/Order/Module/HahnEmbedding.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean

Modified Mathlib/Analysis/AbsoluteValue/Equivalence.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Defs.lean

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

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

Modified Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

Modified Mathlib/Analysis/RCLike/Extend.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

modified theorem CategoryTheory.Grpd.id_eq_id

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

Modified Mathlib/Data/Int/WithZero.lean

Modified Mathlib/Data/Seq/Basic.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/Extension/Presentation/Submersive.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

Modified Mathlib/RingTheory/Ideal/IsPrincipal.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

Modified Mathlib/RingTheory/Polynomial/Wronskian.lean

Modified Mathlib/RingTheory/ReesAlgebra.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/RingTheory/WittVector/Identities.lean

Modified Mathlib/Topology/Algebra/AffineSubspace.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean