X_mul_modMonomial

Mathlib.Algebra.MvPolynomial.Division

URI: https://scilib.ai/kg/mathlib#MvPolynomial.X_mul_modMonomial

English

X_i times x modulo monomial i 1 equals 0.

Русский

X_i умножение на x по модулю мономиала i 1 равно нулю.

LaTeX

$$$X_i \\cdot x \\; \\%^{mon} Finsupp.single i 1 = 0$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru