modMonomial

Mathlib.Algebra.MvPolynomial.Division

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

← MathLib Explorer

English

The remainder upon division by monomial s is given by modMonomial(x,s).

Русский

Остаток при делении по мономиалу s задаётся modMonomial(x,s).

LaTeX

$$$\\operatorname{modMonomial}(x,s) = x \\bmod_{mon} s$$$

Lean4

/-- The remainder upon division by `monomial 1 s`. -/
noncomputable def modMonomial (x : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R :=
  x.modOf s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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