Commit 2024-06-15 21:43 32cac551

View on Github →

chore: tidy various files (#13860)

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

modified theorem LieAlgebra.IsSemisimple.isSimple_of_isAtom

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Modified Mathlib/Analysis/Convex/Body.lean

Modified Mathlib/Analysis/Convex/Slope.lean

Modified Mathlib/Analysis/SumIntegralComparisons.lean

Modified Mathlib/CategoryTheory/Abelian/EpiWithInjectiveKernel.lean

Modified Mathlib/CategoryTheory/Functor/Category.lean

modified theorem CategoryTheory.Iso.map_hom_inv_id_app

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Condensed/Light/Explicit.lean

Modified Mathlib/Data/Nat/Lattice.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/GroupTheory/Perm/List.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

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

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

modified theorem PMF.restrict_toMeasure_support

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/RingTheory/RootsOfUnity/Complex.lean

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

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/TietzeExtension.lean