Commit 2024-07-07 19:14 38e09f6c

View on Github →

chore (BigOperators.Finsupp): avoid importing Order.BigOperators.Ring.Finset (#14336) This is one part of the import path from Algebra.Order.Group.Defs here and clearly unnecessary.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

modified theorem Nat.prod_pow_pos_of_zero_not_mem_support

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

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

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/Combinatorics/Optimization/ValuedCSP.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

modified theorem SimpleGraph.posSemidef_lapMatrix

Modified Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

Modified Mathlib/NumberTheory/Primorial.lean

Modified scripts/noshake.json