Theorems · Theorem · number theory

geom_sum_alternating_of_le_neg_one

∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {x : R},
  x + 1 ≤ 0 → ∀ (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

1 results in Mathlib

Foundations

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

Assumes

RingPartialOrderIsOrderedRing