modByMonic_repr_map

Mathlib.RingTheory.IsAdjoinRoot

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

← MathLib Explorer

English

The representation map commutes with mod by monic: h.repr (h.map g) mod by f equals g mod by f.

Русский

Представление коммутирует modByMonic: h.repr (h.map g) mod f = g mod f.

LaTeX

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

Lean4

theorem modByMonic_repr_map (g : R[X]) : h.repr (h.map g) %ₘ f = g %ₘ f :=
  modByMonic_eq_of_dvd_sub h.monic <| by rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

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

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

Разделы

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

Аффилиация

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