X_dvd_monomial — Mathlib

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]

Похожие утверждения