Theorem one_lt_ite

Modification history

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