Theorems · Theorem · number theory

geom_sum_pos_and_lt_one

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

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

RingPartialOrderIsStrictOrderedRing