Commit 2025-04-14 18:04 7860ff0f

View on Github →

chore: tidy various files (#23975)

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

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

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

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

Modified Mathlib/Computability/ContextFreeGrammar.lean

modified theorem ContextFreeGrammar.derives_nonterminal

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/Matroid/Loop.lean

modified theorem Matroid.eq_loopyOn_iff_loops

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

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/GroupTheory/FreeGroup/Reduce.lean

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/g2.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/UnifTight.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean

Modified Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

Modified Mathlib/Topology/Algebra/Ring/Compact.lean

Modified Mathlib/Topology/Separation/Basic.lean