ker

Mathlib.RingTheory.Ideal.Maps

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

English

The kernel of a ring homomorphism is the comap of ⊥, i.e., ker f = comap f ⊥.

Русский

ядеро гомоморфизма — это comap от нуля: ker f = comap f ⊥.

LaTeX

$$RingHom.ker f = comap f ⊥$$

Lean4

/-- Kernel of a ring homomorphism as an ideal of the domain. -/
def ker : Ideal R :=
  Ideal.comap f ⊥

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

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

Разделы

Аффилиация

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