divMonomial_zero

Mathlib.Algebra.MvPolynomial.Division

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

English

Dividing by monomial with exponent 0 leaves the polynomial unchanged: x / monomial 0 = x.

Русский

Деление по мономиалу степени 0 не меняет полином: x / monomial 0 = x.

LaTeX

$$$\\dfrac{x}{^{mon} 0} = x$$$

Lean4

theorem divMonomial_zero (x : MvPolynomial σ R) : x /ᵐᵒⁿᵒᵐⁱᵃˡ 0 = x :=
  x.divOf_zero

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

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

Разделы

Аффилиация

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