case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r q : R[X]
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * q) n = ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff q x.snd
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p * q) n = ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd
rcases p with ⟨p⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * { toFinsupp := q }) n =
    ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff { toFinsupp := q } x.snd
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r q : R[X]
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * q) n = ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff q x.snd
rcases q with ⟨q⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ ↑(p * q) n = ∑ x in Nat.antidiagonal n, ↑p x.fst * ↑q x.snd
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * { toFinsupp := q }) n =
    ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff { toFinsupp := q } x.snd
simp_rw [← ofFinsupp_mul, coeff]
no goals
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ ↑(p * q) n = ∑ x in Nat.antidiagonal n, ↑p x.fst * ↑q x.snd
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Nat.mem_antidiagonal