case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
w : natDegree p < n
⊢ sum p f = ∑ a in range n, f a (coeff p a)
rcases p with ⟨⟩
case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : support { toFinsupp := toFinsupp✝ } ⊆ range n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
have := supp_subset_range w
case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : toFinsupp✝.support ⊆ range n
⊢ ∑ x in toFinsupp✝.support, f x (↑toFinsupp✝ x) = ∑ x in range n, f x (↑toFinsupp✝ x)
case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : support { toFinsupp := toFinsupp✝ } ⊆ range n
⊢ sum { toFinsupp := toFinsupp✝ } f = ∑ a in range n, f a (coeff { toFinsupp := toFinsupp✝ } a)
simp only [Polynomial.sum, support, coeff, natDegree, degree] at this⊢
no goals
case ofFinsupp
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
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
w : natDegree { toFinsupp := toFinsupp✝ } < n
this : toFinsupp✝.support ⊆ range n
⊢ ∑ x in toFinsupp✝.support, f x (↑toFinsupp✝ x) = ∑ x in range n, f x (↑toFinsupp✝ x)
exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n