English
For i, j and r in a MV-polynomial framework, X_i divides monomial j r iff either r = 0 or the i-th coordinate of j is nonzero.
Русский
Для mономиалов X_i делит мономиал j r тогда и только тогда, когда либо r = 0, либо i-ая координата j не ноль.
LaTeX
$$$$ X_i \\mid \\text{monomial}(j,r) \\iff r = 0 \\lor j(i) \\neq 0. $$$$
Lean4
@[simp]
theorem X_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} : (X i : MvPolynomial σ R) ∣ monomial j r ↔ r = 0 ∨ j i ≠ 0 :=
by
refine monomial_dvd_monomial.trans ?_
simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]