Commit 2026-02-10 17:28 9c01b6b2

View on Github →

chore(Algebra/Order/GroupWithZero): generalize some hypotheses from pos to nonneg (#34992)

Estimated changes

modified theorem Finset.mul₀_sup'
modified theorem Finset.sup'_div₀
modified theorem Finset.sup'_mul₀
modified theorem Finset.sup_div₀