R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ i in range (n + 1), ↑(lcoeff R k) (X ^ i * ↑C r ^ (n - i) * ↑(Nat.choose n i)) = r ^ (n - k) * ↑(Nat.choose n k)
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ coeff ((X + ↑C r) ^ n) k = r ^ (n - k) * ↑(Nat.choose n k)
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, LinearMap.map_sum]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ x in range (n + 1), coeff (X ^ x) k * r ^ (n - x) * ↑(Nat.choose n x) = r ^ (n - k) * ↑(Nat.choose n k)
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ i in range (n + 1), ↑(lcoeff R k) (X ^ i * ↑C r ^ (n - i) * ↑(Nat.choose n i)) = r ^ (n - k) * ↑(Nat.choose n k)
simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_nat_cast, ← C_pow, coeff_mul_C, Nat.cast_id]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∀ (b : ℕ), b ∈ range (n + 1) → b ≠ k → coeff (X ^ b) k * r ^ (n - b) * ↑(Nat.choose n b) = 0

case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ¬k ∈ range (n + 1) → coeff (X ^ k) k * r ^ (n - k) * ↑(Nat.choose n k) = 0
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ x in range (n + 1), coeff (X ^ x) k * r ^ (n - x) * ↑(Nat.choose n x) = r ^ (n - k) * ↑(Nat.choose n k)
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ coeff (X ^ b✝) k * r ^ (n - b✝) * ↑(Nat.choose n b✝) = 0
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∀ (b : ℕ), b ∈ range (n + 1) → b ≠ k → coeff (X ^ b) k * r ^ (n - b) * ↑(Nat.choose n b) = 0
intro _ _ h
no goals
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ coeff (X ^ b✝) k * r ^ (n - b✝) * ↑(Nat.choose n b✝) = 0
simp [coeff_X_pow, h.symm]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(Nat.choose n k) = 0
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ¬k ∈ range (n + 1) → coeff (X ^ k) k * r ^ (n - k) * ↑(Nat.choose n k) = 0
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(Nat.choose n k) = 0
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(Nat.choose n k) = 0
intro h
no goals
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(Nat.choose n k) = 0
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]