Commit 2025-03-14 12:06 3afb0299

View on Github →

chore: tidy various files (#22894)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

modified def DirectSum.map

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem enorm_eq_zero'

modified theorem enorm_ne_zero'

modified theorem enorm_pos'

Modified Mathlib/Analysis/Normed/Group/Continuity.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

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

Modified Mathlib/CategoryTheory/Monoidal/Yoneda.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean

Modified Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Set/FunctorToTypes.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean

Modified Mathlib/MeasureTheory/Function/FactorsThrough.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

modified theorem ArithmeticFunction.mul_zeta_apply

modified theorem ArithmeticFunction.zeta_mul_apply

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Modified Mathlib/RingTheory/Polynomial/SmallDegreeVieta.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean