Theorems · Theorem · number theory

geom_sum_alternating_of_lt_neg_one

∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  x + 1 < 0 → 1 < n → if Even n then ∑ i ∈ Finset.range n, x ^ i < 0 else 1 < ∑ i ∈ Finset.range n, x ^ i

Defined in

Mathlib.Algebra.Order.Ring.GeomSum

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingPartialOrderIsStrictOrderedRing