min_max): `a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂` (#18667)

Commit

2 years ago

feat(algebra/order/monoid/min_max): `a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂` (#18667) Complete the API.

Author

YaelDillies

Parents