monomial_modMonomial

Mathlib.Algebra.MvPolynomial.Division

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

English

Monomial s 1 modulo s is zero: monomial s 1 /ᵐᵒⁿᵒᵐⁱᵃˡ s = 0.

Русский

Мономиал s 1 по модулю s даёт 0.

LaTeX

$$$\\operatorname{monomial}(s)\\;1 /^{mon} s = 0$$$

Lean4

@[simp]
theorem monomial_modMonomial (s : σ →₀ ℕ) : monomial s (1 : R) %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  AddMonoidAlgebra.of'_modOf _

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

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

Разделы

Аффилиация

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