modByMonicHom_map

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRootMonic.modByMonicHom_map

English

The linear map h.modByMonicHom sends the image of h.map g to g mod f, i.e., h.modByMonicHom (h.map g) = g mod f.

Русский

Линейное отображение modByMonicHom отправляет образ h.map g в g mod f, т.е. h.modByMonicHom (h.map g) = g mod f.

LaTeX

$$$ h.modByMonicHom (h.map g) = g \bmod f $$$

Lean4

@[simp]
theorem modByMonicHom_map (g : R[X]) : h.modByMonicHom (h.map g) = g %ₘ f :=
  h.modByMonic_repr_map g

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

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

Разделы

Аффилиация

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