X_divMonomial

Mathlib.Algebra.MvPolynomial.Division

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

English

X_i divided by monomial Finsupp.single i 1 equals 1.

Русский

X_i делится по мономиалу i 1 на единицу.

LaTeX

$$$(X_i) /^{mon} Finsupp.single i 1 = 1$$$

Lean4

@[simp]
theorem X_divMonomial (i : σ) : (X i : MvPolynomial σ R) /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 1 :=
  divMonomial_monomial (Finsupp.single i 1)

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

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

Разделы

Аффилиация

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