Commit 2022-10-19 07:31 e891db24

View on Github →

feat: port Init/Algebra/Classes.lean (#476)

Estimated changes

added theorem antisymm
added theorem asymm
added theorem asymm_of
added theorem eq_of_eqv_lt
added theorem eq_of_incomp
added theorem eqv_lt_iff_eq
added theorem incomp_iff_eq
added theorem incomp_trans
added theorem incomp_trans_of
added theorem irrefl
added theorem irrefl_of
added theorem lt_of_incomp_of_lt
added theorem lt_of_lt_of_incomp
added theorem not_lt_of_lt
added theorem refl
added theorem refl_of
added theorem symm
added theorem symm_of
added theorem total_of
added theorem trans
added theorem trans_of
added theorem trichotomous
added theorem trichotomous_of