diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean
index 2ff32cf3159f4..e956f8de346e6 100644
--- 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