Theorems · Theorem · commutative algebra

Polynomial.geom_sum_X_comp_X_add_one_eq_sum

∀ {R : Type u} [inst : Semiring R] (n : ℕ),
  (∑ i ∈ Finset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) =
    ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * Polynomial.X ^ i

Defined in: Mathlib.RingTheory.Polynomial.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites24

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Semiringstatement and proof · cited by 13,802
Polynomialstatement · cited by 5,681
Finset.sumstatement and proof · cited by 5,195
Finset.sum_congrproof · cited by 2,323
Nat.cast_zeroproof · cited by 1,870
Polynomial.Xstatement and proof · cited by 1,639
Polynomial.Cproof · cited by 1,598
Finset.rangestatement and proof · cited by 1,341
Polynomial.coeffproof · cited by 1,045
Nat.cast_addproof · cited by 586
Nat.choosestatement and proof · cited by 494

Cited by1

Results whose statement or proof uses this declaration.

cyclotomic_comp_X_add_one_isEisensteinAtproof · cited by 1