Polynomial (1 + X) ^ n - 1

This file contains results on polynomial (1 + X) ^ n - 1. Mathematically, it is viewed as the multiply-by-n map [n] of the formal multiplicative group $\widehat{\mathbb{G}}_m$. In particular, (1 + X) ^ p ^ n - 1 is a distinguished polynomial at p, and the ideal generated by p ^ m and it are cofinal with (p ^ m, X ^ n) (Polynomial.oneAddXPowSubOne_mem_span_natCast_X_pow and Polynomial.span_natCast_X_pow_le_span_natCast_pow_oneAddXPowSubOne).

noncomputable def Polynomial.oneAddXPowSubOne (R : Type u_1) (n : ℕ) [Semiring R] : Polynomial R

The Polynomial.oneAddXPowSubOne R n is the polynomial (1 + X) ^ n - 1 in R[X] (Polynomial.oneAddXPowSubOne_def). Since we allow R to be a Semiring, its actual definition is ∑ i ∈ [1, n + 1), X ^ i * n.choose i.

Equations

• Polynomial.oneAddXPowSubOne R n = ∑ i ∈ Finset.Ico 1 (n + 1), Polynomial.X ^ i * ↑(n.choose i)

@[simp]

theorem Polynomial.oneAddXPowSubOne_zero (R : Type u_1) [Semiring R] : oneAddXPowSubOne R 0 = 0

@[simp]

theorem Polynomial.oneAddXPowSubOne_one (R : Type u_1) [Semiring R] : oneAddXPowSubOne R 1 = X

theorem Polynomial.oneAddXPowSubOne_eq_map (R : Type u_1) (n : ℕ) [Semiring R] : oneAddXPowSubOne R n = map (algebraMap ℕ R) (oneAddXPowSubOne ℕ n)

theorem Polynomial.commute_oneAddXPowSubOne (R : Type u_1) (n : ℕ) [Semiring R] (p : Polynomial R) : Commute (oneAddXPowSubOne R n) p

theorem Polynomial.coeff_oneAddXPowSubOne_eq (R : Type u_1) (n : ℕ) [Semiring R] (i : ℕ) : (oneAddXPowSubOne R n).coeff i = if i = 0 then 0 else ↑(n.choose i)

theorem Polynomial.coeff_oneAddXPowSubOne_eq_one_of_ne_zero (R : Type u_1) (n : ℕ) [Semiring R] (hn : n ≠ 0) : (oneAddXPowSubOne R n).coeff n = 1

theorem Polynomial.degree_oneAddXPowSubOne_of_ne_zero (R : Type u_1) (n : ℕ) [Semiring R] [Nontrivial R] (hn : n ≠ 0) : (oneAddXPowSubOne R n).degree = ↑n

theorem Polynomial.natDegree_oneAddXPowSubOne (R : Type u_1) (n : ℕ) [Semiring R] [Nontrivial R] : (oneAddXPowSubOne R n).natDegree = n

theorem Polynomial.monic_oneAddXPowSubOne_of_ne_zero (R : Type u_1) (n : ℕ) [Semiring R] (hn : n ≠ 0) : (oneAddXPowSubOne R n).Monic

theorem Polynomial.oneAddXPowSubOne_def (R : Type u_1) (n : ℕ) [Ring R] : oneAddXPowSubOne R n = (1 + X) ^ n - 1

theorem Polynomial.oneAddXPowSubOne_mul_geom_sum (R : Type u_1) (n : ℕ) [Semiring R] (m : ℕ) : oneAddXPowSubOne R n * ∑ i ∈ Finset.range m, (1 + X) ^ (n * i) = oneAddXPowSubOne R (n * m)

theorem Polynomial.oneAddXPowSubOne_dvd_of_dvd (R : Type u_1) (n : ℕ) [Semiring R] (m : ℕ) (h : n ∣ m) : oneAddXPowSubOne R n ∣ oneAddXPowSubOne R m

theorem Polynomial.X_dvd_oneAddXPowSubOne (R : Type u_1) (n : ℕ) [Semiring R] : X ∣ oneAddXPowSubOne R n

theorem Polynomial.dvd_coeff_oneAddXPowSubOne_of_ne (R : Type u_1) (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [Semiring R] (i : ℕ) (hi : i ≠ p ^ n) : ↑p ∣ (oneAddXPowSubOne R (p ^ n)).coeff i

theorem Polynomial.oneAddXPowSubOne_mem_span_natCast_X_pow (R : Type u_1) (p n : ℕ) [Semiring R] : oneAddXPowSubOne R (p ^ n) ∈ Ideal.span {↑p, X} ^ (n + 1)

theorem Polynomial.test1_isTwoSided (R : Type u_1) [Semiring R] (Y : Polynomial R) (hY : ∀ (q : Polynomial R), Commute Y q) (Z : Polynomial R) (hZ : ∀ (q : Polynomial R), Commute Z q) : (Ideal.span {Y, Z}).IsTwoSided

theorem Polynomial.test1_le (R : Type u_1) [Semiring R] (m : ℕ) (hm : m ≠ 0) (Y : Polynomial R) (hY : ∀ (q : Polynomial R), Commute Y q) (Z : Polynomial R) (hZ : ∀ (q : Polynomial R), Commute Z q) : Ideal.span {Y, Z} ^ m ≤ Ideal.span {Y, Z ^ m}

theorem Polynomial.X_pow_natCast_pow_mem_span_natCast_oneAddXPowSubOne (R : Type u_1) (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [Ring R] : X ^ p ^ n ∈ Ideal.span {↑p, oneAddXPowSubOne R (p ^ n)}

theorem Polynomial.span_natCast_X_pow_natCast_pow_le_span_natCast_oneAddXPowSubOne (R : Type u_1) (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [Ring R] : Ideal.span {↑p, X} ^ p ^ n ≤ Ideal.span {↑p, oneAddXPowSubOne R (p ^ n)}

theorem Ideal.IsTwoSided.pow_mul {R : Type u_2} [Semiring R] {I : Ideal R} [I.IsTwoSided] (m n : ℕ) : I ^ (m * n) = (I ^ m) ^ n

theorem Polynomial.span_natCast_X_pow_le_span_natCast_pow_oneAddXPowSubOne (R : Type u_1) (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [Ring R] (m k : ℕ) (hm : m ≠ 0) (hk : k ≥ p ^ n * m) : Ideal.span {↑p, X} ^ k ≤ Ideal.span {↑p ^ m, oneAddXPowSubOne R (p ^ n)}

theorem Polynomial.isDistinguishedAt_oneAddXPowSubOne (R : Type u_1) (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CommRing R] : (oneAddXPowSubOne R (p ^ n)).IsDistinguishedAt (Ideal.span {↑p})