Commit 2024-10-20 12:53 d1729028

View on Github →

chore(Algebra/Order/BigOperators/Group/Finset): don't import Ring (#17939) By moving the positivity extension, one can shave off a bunch of imports

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

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

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

deleted def Mathlib.Meta.Positivity.evalFinsetSum

Modified Mathlib/Algebra/Order/Chebyshev.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/Complex/AbelLimit.lean

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

Modified Mathlib/Combinatorics/Enumerative/DoubleCounting.lean

Modified Mathlib/Combinatorics/Pigeonhole.lean

Modified Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/Nat/Choose/Sum.lean

Modified Mathlib/Data/Set/Equitable.lean

Modified Mathlib/Data/Sign.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/Harmonic/Defs.lean

Modified Mathlib/Order/Partition/Equipartition.lean

Modified Mathlib/Tactic/Positivity/Finset.lean

added def Mathlib.Meta.Positivity.evalFinsetSum

Modified Mathlib/Testing/SlimCheck/Functions.lean

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

Modified scripts/noshake.json

Modified test/positivity.lean