Theorem dite_lt_one

Modification history

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