Commit 2024-12-21 19:08 c758509f

View on Github →

chore: tidy various files (#20154)

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

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

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

Modified Mathlib/Algebra/Homology/Bifunctor.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Convex/Continuous.lean

Modified Mathlib/Analysis/Convex/KreinMilman.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthonormal.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

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

Modified Mathlib/Analysis/Normed/Ring/Seminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

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

Modified Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/LSeries/Convergence.lean

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

Modified Mathlib/Order/Defs/LinearOrder.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Zorn.lean

Modified Mathlib/RingTheory/Radical.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

modified def TwoSidedIdeal.comap

Modified Mathlib/RingTheory/Unramified/Basic.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/Topology/Algebra/Nonarchimedean/TotallyDisconnected.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem eq_singleton_left_of_prod_subset_idRel

modified theorem eq_singleton_prod_subset_idRel

modified theorem eq_singleton_right_prod_subset_idRel

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

modified theorem UniformSpace.DiscreteUnif.cauchy_le_pure

modified theorem UniformSpace.DiscreteUnif.eq_const_of_cauchy