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