mathlib
633c32ea - feat(order/basic): Checking associativity in partial order (#17942)

Commit

3 years ago

feat(order/basic): Checking associativity in partial order (#17942) Simpler conditions to check commutativity/associativity of a function valued in a partial order.

Author

YaelDillies

Parents

4237da0f

mathlib 633c32ea - feat(order/basic): Checking associativity in partial order (#17942)

mathlib
633c32ea - feat(order/basic): Checking associativity in partial order (#17942)