Theorems · Theorem · number theory

geom_sum_neg_iff

∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  n ≠ 0 → (∑ i ∈ Finset.range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0)

Defined in

Mathlib.Algebra.Order.Ring.GeomSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderIsStrictOrderedRing