Theorems · Theorem · order theory

nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg

∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R],
  0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Defined in

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

SemiringLinearOrderMulPosStrictMonoPosMulStrictMono