Commit 2026-03-03 22:45 9c13d4dd

View on Github →

chore(Algebra/Order/BigOperators): move lemmas which don't use addition out of Ring (#35005) These lemmas all use no addition or additive operations whatsoever, so we move them out of Ring/ and into GroupWithZero. This is more consistent with the existing pattern in Algebra/BigOperators, and aids searchability. This PR also golfs and generalises Finset.one_le_prod. This could be a separate PR, but note that this change requires the move made in this PR, so it seems easier to combine the changes.

Estimated changes

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

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

added theorem Finset.le_prod_max_one

modified theorem Finset.one_le_prod

added theorem Finset.prod_le_one

added theorem Finset.prod_le_prod

added theorem Finset.prod_lt_prod

added theorem Finset.prod_lt_prod_of_nonempty

added theorem Finset.prod_nonneg

added theorem Finset.prod_pos

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

deleted theorem Finset.le_prod_max_one

deleted theorem Finset.prod_le_one

deleted theorem Finset.prod_le_prod

deleted theorem Finset.prod_lt_prod

deleted theorem Finset.prod_lt_prod_of_nonempty

deleted theorem Finset.prod_nonneg

deleted theorem Finset.prod_pos

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Analysis/Convex/NNReal.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Data/NNRat/BigOperators.lean

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

Modified Mathlib/NumberTheory/Primorial.lean

Modified Mathlib/Topology/Metrizable/ContinuousMap.lean