case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ n ∈ support { toFinsupp := toFinsupp✝ } ↔ coeff { toFinsupp := toFinsupp✝ } n ≠ 0
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n ∈ support p ↔ coeff p n ≠ 0
rcases p with ⟨⟩
no goals
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ n ∈ support { toFinsupp := toFinsupp✝ } ↔ coeff { toFinsupp := toFinsupp✝ } n ≠ 0
simp