mem_ker_map

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.mem_ker_map

English

The kernel of h.map is generated by f, i.e., a polynomial p lies in ker(h.map) iff f divides p.

Русский

Ядро отображения h.map состоит порождается F, то есть p ∈ ker(h.map) тогда и только тогда, когда f делит p.

LaTeX

$$$p \\in \\ker(h.map) \\iff f \\mid p$$$

Lean4

theorem mem_ker_map {p} : p ∈ RingHom.ker h.map ↔ f ∣ p := by rw [h.ker_map, Ideal.mem_span_singleton]

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

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

Разделы

Аффилиация

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