Commit 2024-08-26 10:46 52fdd961

View on Github →

chore: tidy various files (#16132)

Estimated changes

Modified Archive/Sensitivity.lean

modified theorem Sensitivity.f_squared

Modified Counterexamples/Phillips.lean

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

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

Modified Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean

Modified Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

Modified Mathlib/Data/Finset/Lattice.lean

Modified Mathlib/Data/List/Sort.lean

modified theorem List.mem_insertionSort

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/MeasureTheory/Decomposition/Exhaustion.lean

Modified Mathlib/ModelTheory/Fraisse.lean

Modified Mathlib/ModelTheory/PartialEquiv.lean

modified theorem FirstOrder.Language.DirectLimit.le_partialEquivLimit

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Order/SuccPred/LinearLocallyFinite.lean

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/RingTheory/Derivation/ToSquareZero.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/MvPolynomial/Localization.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

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

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean