case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑{ toFinsupp := toFinsupp✝ }.toFinsupp i = coeff { toFinsupp := toFinsupp✝ } i
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q f : R[X]
i : ℕ
⊢ ↑f.toFinsupp i = coeff f i
cases f
no goals
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑{ toFinsupp := toFinsupp✝ }.toFinsupp i = coeff { toFinsupp := toFinsupp✝ } i
rfl