Theorem Finset.sup'_div₀

Modification history

2026-02-10 17:28

Mathlib/Algebra/Order/GroupWithZero/Finset.lean

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

Modified Finset.sup'_div₀ View on Github →

2025-04-11 08:18

Mathlib/Algebra/Order/GroupWithZero/Finset.lean

feat(Order/GroupWithZero): drop more TC assumptions (#23922) …

Modified Finset.sup'_div₀ View on Github →

2025-04-10 02:58

Mathlib/Algebra/Order/GroupWithZero/Finset.lean

feat(Order/GroupWithZero): drop some `0 ≤ 1` assumptions (#23892) …

Modified Finset.sup'_div₀ View on Github →

2024-11-25 17:02

Mathlib/Algebra/Order/GroupWithZero/Finset.lean

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

Added Finset.sup'_div₀ View on Github →