case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f

case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
by_cases hp : p = 0
no goals
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : ¬p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
  Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∀ (x : Fin n), x ∈ univ → f (↑x) (coeff 0 ↑x) = 0
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∑ i : Fin n, f (↑i) (coeff p ↑i) = sum p f
rw [hp, sum_zero_index, Finset.sum_eq_zero]
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
⊢ ∀ (x : Fin n), x ∈ univ → f (↑x) (coeff 0 ↑x) = 0
intro i _
no goals
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : degree p < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0
exact hf i