ker_le_comap

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.ker_le_comap

English

The kernel of a RingHom f is contained in the comap of any ideal K along f.

Русский

Ядро отображения f входит в comap любого идеала K по отображению f.

LaTeX

$$$ \\operatorname{ker} f \\le \\operatorname{comap} f K. $$$

Lean4

theorem ker_le_comap {K : Ideal S} (f : F) : RingHom.ker f ≤ comap f K := fun _ hx =>
  mem_comap.2 (RingHom.mem_ker.1 hx ▸ K.zero_mem)

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

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

Разделы

Аффилиация

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