Commit 2023-05-24 01:45 de301c80

View on Github →

feat: port Init.Data.Ordering.Lemmas (#4281)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/Data/Ordering/Lemmas.lean

added theorem Ordering.ite_eq_eq_distrib

added theorem Ordering.ite_eq_gt_distrib

added theorem Ordering.ite_eq_lt_distrib

added theorem cmpUsing_eq_eq

added theorem cmpUsing_eq_gt

added theorem cmpUsing_eq_lt