mul_X_modMonomial — Mathlib

English

Let R be a commutative semiring and σ a type. For every polynomial x in MvPolynomial(σ, R) and every i in σ, the product x · X_i is divisible by the monomial X_i of degree 1 in the i-th variable; equivalently, the remainder upon division of x · X_i by X_i is 0.

Русский

Пусть R — коммутативная полупрямой кольцо, σ — множество. Для любого многочлена x ∈ MvPolynomial(σ, R) и любого i ∈ σ произведение x · X_i делится на моном X_i степени 1 по переменной i; эквивалентно, остаток от деления x · X_i по мономиалу X_i равен 0.

LaTeX

$$$$ X_i \mid x X_i. $$$$

Lean4

@[simp]
theorem mul_X_modMonomial (x : MvPolynomial σ R) (i : σ) : x * X i %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0 :=
  mul_monomial_modMonomial _ _

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