feat: MvPolynomial.X_ne_zero (#11071)

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

Mathlib/Data/MvPolynomial/Basic.lean

@@ -818,6 +818,13 @@ theorem ne_zero_iff {p : MvPolynomial σ R} : p ≠ 0 ↔ ∃ d, coeff d p ≠ 0
   rfl
 #align mv_polynomial.ne_zero_iff MvPolynomial.ne_zero_iff
 
+@[simp]
+theorem X_ne_zero [Nontrivial R] (s : σ) :
+    X (R := R) s ≠ 0 := by
+  rw [ne_zero_iff]
+  use Finsupp.single s 1
+  simp only [coeff_X, ne_eq, one_ne_zero, not_false_eq_true]
+
 @[simp]
 theorem support_eq_empty {p : MvPolynomial σ R} : p.support = ∅ ↔ p = 0 :=
   Finsupp.support_eq_empty