ker_eq_comap_bot

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingHom.ker_eq_comap_bot

English

The kernel of f is equal to the comap of the bottom ideal along f, i.e., ker f = Ideal.comap f ⊥.

Русский

Ядро f равно обратному образу нулевого идеала по отображению f, то есть ker f = Ideal.comap f ⊥.

LaTeX

$$$\\ker f = \\mathrm{Ideal.comap}\n f \\bot$$$

Lean4

theorem ker_eq_comap_bot (f : F) : ker f = Ideal.comap f ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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