R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (if 0 = 0 then 1 else 0) = 1
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff 1 0 = 1
rw [← monomial_zero_one, coeff_monomial]
no goals
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (if 0 = 0 then 1 else 0) = 1
simp