case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
p q : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = coeff { toFinsupp := q } → { toFinsupp := p } = { toFinsupp := q }
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Injective coeff
rintro ⟨p⟩ ⟨q⟩
no goals
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
p q : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = coeff { toFinsupp := q } → { toFinsupp := p } = { toFinsupp := q }
simp only [coeff, FunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]