map_modByMonicHom

Mathlib.RingTheory.IsAdjoinRoot

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

English

Unicity of modByMonicHom: h.modByMonicHom (h.map g) = g mod f for all g ∈ R[X].

Русский

Уникальность modByMonicHom: для любого g ∈ R[X] верно h.modByMonicHom (h.map g) = g mod f.

LaTeX

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

Lean4

@[simp]
theorem map_modByMonicHom (x : S) : h.map (h.modByMonicHom x) = x := by simp [modByMonicHom, map_modByMonic, map_repr]

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

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

Разделы

Аффилиация

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