modMonomial_X — Mathlib

English

In the multivariable polynomial ring, the monomial X_i is divisible by the monomial X_i itself; i.e., X_i ∣ X_i.

Русский

В кольце многочленов с несколькими переменными моном X_i делится на сам моном X_i; то есть X_i ∣ X_i.

LaTeX

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

Lean4

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

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