Theorems · Theorem · order theory

mul_nonpos_iff

∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R], a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingLinearOrderMulPosStrictMonoPosMulStrictMonoAddLeftReflectLEAddLeftMono