Commit 2024-11-25 17:02 25781872

View on Github →

feat: Finset.sup in a group with zero (#19461)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/GroupWithZero/Finset.lean

added theorem Finset.inf'_mul_le_mul_inf'_of_nonneg

added theorem Finset.mul_inf_le_inf_mul_of_nonneg

added theorem Finset.mul₀_sup'

added theorem Finset.sup'_div₀

added theorem Finset.sup'_mul_le_mul_sup'_of_nonneg

added theorem Finset.sup'_mul₀

added theorem Finset.sup_div₀

added theorem Finset.sup_mul_le_mul_sup_of_nonneg

Deleted Mathlib/Algebra/Order/Ring/Finset.lean

deleted theorem Finset.inf'_mul_le_mul_inf'_of_nonneg

deleted theorem Finset.mul_inf_le_inf_mul_of_nonneg

deleted theorem Finset.sup'_mul_le_mul_sup'_of_nonneg

deleted theorem Finset.sup_mul_le_mul_sup_of_nonneg

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean