monomial_one_dvd_iff_modMonomial_eq_zero

English

Monomial i 1 divides x if and only if x modulo monomial i 0 equals zero.

Русский

Мономиал i 1 делит x тогда и только тогда, когда x mod мономиал i 0 равен нулю.

LaTeX

$$$\\monomial(i)\\,1 \\mid x \\; \\Leftrightarrow \\ x \\equiv 0 \\; (\\bmod_{mon} i)$$$

Lean4

theorem monomial_one_dvd_iff_modMonomial_eq_zero {i : σ →₀ ℕ} {x : MvPolynomial σ R} :
    monomial i (1 : R) ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ i = 0 :=
  AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero

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