X_dvd_iff_modMonomial_eq_zero — Mathlib

English

An element X_i divides a polynomial x if and only if the remainder after dividing by the monomial with exponent 1 at i is zero.

Русский

Секция X_i делит многочлен x тогда и только тогда, когда остаток после деления на мономiал с единичной степенью по i равен нулю.

LaTeX

$$$$ X_i \\mid x \\;\\iff\\; x \\bmod \\text{monomial}(Finsupp.single i 1) = 0. $$$$

Lean4

theorem X_dvd_iff_modMonomial_eq_zero {i : σ} {x : MvPolynomial σ R} : X i ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  monomial_one_dvd_iff_modMonomial_eq_zero

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