Theorem one_le_dite

Modification history

2025-01-16 00:33
Mathlib/Algebra/ZeroOne/Lemmas.lean
chore: move Algebra/Group/ZeroOne/ to Data/ (#20622) …
Modified one_le_diteView on Github →
2023-09-28 21:41
Mathlib/Order/Basic.lean
feat: Extend a nonnegative function (#7418) …
Added one_le_diteView on Github →