Theorem Ordering.ite_eq_lt_distrib

Modification history

2023-05-24 01:45
Mathlib/Init/Data/Ordering/Lemmas.lean
feat: port Init.Data.Ordering.Lemmas (#4281)
Added Ordering.ite_eq_lt_distribView on Github →