Commit 2022-12-15 10:44 9b60f00e

View on Github →

feat: Checking associativity in partial order (#1030) Match https://github.com/leanprover-community/mathlib/pull/17942

Estimated changes

Modified Mathlib/Order/Basic.lean

added theorem associative_of_commutative_of_le

added theorem commutative_of_le