Commit 2024-12-21 08:53 f63994b7

View on Github →

chore: tidy various files (#20130)

Estimated changes

Modified Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Field/Subfield/Basic.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

modified theorem Nat.finMulAntidiag_three

Modified Mathlib/Algebra/Order/Quantale.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Analysis/Analytic/IteratedFDeriv.lean

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

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/Data/List/Intervals.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

modified theorem CommGroup.exists_apply_ne_one_aux

Modified Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

Modified Mathlib/Probability/Kernel/Composition/ParallelComp.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

modified theorem Polynomial.Monic.quotient_isIntegral

Modified Mathlib/Topology/UniformSpace/HeineCantor.lean