monomial_mul_modMonomial

Mathlib.Algebra.MvPolynomial.Division

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

English

Monomial s 1 times x modulo s equals 0.

Русский

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

LaTeX

$$$\\operatorname{monomial}(s)\\;1 \\cdot x \\;\\%^{mon} s = 0$$$

Lean4

@[simp]
theorem monomial_mul_modMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) : monomial s 1 * x %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  x.of'_mul_modOf _

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

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

Разделы

Аффилиация

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