modByMonicHom_mk

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.modByMonicHom_mk

English

For a monic g and f ∈ R[X], the remainder map on the class mk g f yields the remainder f mod g.

Русский

Для монического g и f ∈ R[X] отображение остатка на классе mk g f дает остаток f mod g.

LaTeX

$$modByMonicHom(hg)(mk g f) = f %ₘ g$$

Lean4

@[simp]
theorem modByMonicHom_mk (hg : g.Monic) (f : R[X]) : modByMonicHom hg (mk g f) = f %ₘ g :=
  rfl

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

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

Разделы

Аффилиация

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