Theorems · Theorem · order theory

mul_neg_iff

∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftReflectLT R] [AddLeftStrictMono 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

RingLinearOrderPosMulStrictMonoMulPosStrictMonoAddLeftReflectLTAddLeftStrictMono