Theorem bddAbove_range_mul

Modification history

2025-01-16 10:39
Mathlib/Algebra/Order/GroupWithZero/Bounds.lean
feat: split Mathlib/Algebra/Order/Ring/Unbundled/Nonneg (#20703) …
Modified bddAbove_range_mulView on Github →
2025-01-13 15:16
Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean
feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas (#18172) …
Added bddAbove_range_mulView on Github →