mul_X_divMonomial

Mathlib.Algebra.MvPolynomial.Division

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

English

x multiplied by X_i, then divided by monomial i 1, yields x.

Русский

x умножить на X_i, затем разделить по мономиалу i 1 даёт x.

LaTeX

$$$x \\cdot X_i /^{mon} Finsupp.single i 1 = x$$$

Lean4

@[simp]
theorem mul_X_divMonomial (x : MvPolynomial σ R) (i : σ) : x * X i /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x :=
  divMonomial_mul_monomial _ _

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

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

Разделы

Аффилиация

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