simple polynomial

Stream: new members

[vxctyxeha]

how to solve this problem

import Mathlib
open Polynomial
attribute [local simp] coeff_X
lemma coeff : Polynomial.coeff (1 : ℤ[X]) 2 = 0 := by

[Ruben Van de Velde]

What have you tried?

[Bolton Bailey]

This works:

import Mathlib
open Polynomial
attribute [local simp] coeff_X
lemma coeff : Polynomial.coeff (1 : ℤ[X]) 2 = 0 := by
  have : (1 : ℤ[X]) = Polynomial.C 1 := by exact rfl
  rw [this, Polynomial.coeff_C]
  simp