Theorems · Theorem · order theory

pos_and_pos_or_neg_and_neg_of_mul_pos

∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α] [MulPosMono α],
  0 < a * b → 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Defined in

Mathlib.Algebra.Order.GroupWithZero.Basic

Cited by

3 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

MulZeroClassLinearOrderPosMulMonoMulPosMono