Commit 2025-04-28 20:03 ab000e4c

View on Github →

chore: tidy various files (#24420)

Estimated changes

Modified Mathlib/Algebra/Homology/GrothendieckAbelian.lean

Modified Mathlib/Algebra/Module/End.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/Algebra/Order/Monoid/Prod.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/CategoryTheory/Adjunction/Mates.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Prod.lean

Modified Mathlib/Data/Finsupp/AList.lean

Modified Mathlib/Data/List/Cycle.lean

modified theorem Cycle.not_mem_nil

Modified Mathlib/Data/Matroid/Basic.lean

modified def Matroid.ExchangeProperty

modified def Matroid.ExistsMaximalSubsetProperty

modified structure Matroid

Modified Mathlib/Data/Nat/Fib/Basic.lean

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/Data/Nat/MaxPowDiv.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/NumberTheory/Ostrowski.lean

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean