divMonomial_monomial

Mathlib.Algebra.MvPolynomial.Division

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

English

Monomial a 1 divided by monomial a 1 equals 1.

Русский

monomial a 1 делится на monomial a 1 давая 1.

LaTeX

$$$\\operatorname{divMonomial}(a) = 1$$$

Lean4

@[simp]
theorem divMonomial_monomial (a : σ →₀ ℕ) : monomial a 1 /ᵐᵒⁿᵒᵐⁱᵃˡ a = (1 : MvPolynomial σ R) :=
  AddMonoidAlgebra.of'_divOf _

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

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

Разделы

Аффилиация

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