Commit 2023-07-15 09:21 03458219

View on Github →

chore: re-port Init.Algebra.Classes (#5857) Mainly this adds align statements that were missing, and the header comment.

Estimated changes

Modified Mathlib/Init/Algebra/Classes.lean

added def StrictWeakOrder.Equiv

added theorem StrictWeakOrder.erefl

added theorem StrictWeakOrder.esymm

added theorem StrictWeakOrder.etrans

added theorem StrictWeakOrder.not_lt_of_equiv'

added theorem StrictWeakOrder.not_lt_of_equiv

modified theorem isStrictWeakOrder_of_isTotalPreorder