chore: add simp to Polynomial.X_ne_zero (#11101)

As requested [here](#11071 (comment)) by @riccardobrasca
leanprover-community · Mar 2, 2024 · 0eb97a5 · 0eb97a5
1 parent 5112b8d
commit 0eb97a5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean
@@ -1254,6 +1254,7 @@ instance nontrivial : Nontrivial R[X] := by
   simp [hxy]
 #align polynomial.nontrivial Polynomial.nontrivial
 
+@[simp]
 theorem X_ne_zero : (X : R[X]) ≠ 0 :=
   mt (congr_arg fun p => coeff p 1) (by simp)
 #align polynomial.X_ne_zero Polynomial.X_ne_zero