Theorems · Theorem · order theory

Odd.pow_nonpos_iff

∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → (a ^ n ≤ 0 ↔ a ≤ 0)

Defined in

Mathlib.Algebra.Order.Ring.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringLinearOrderIsStrictOrderedRingExistsAddOfLE