ker_coe_toRingHom

Mathlib.RingTheory.Ideal.Maps

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

English

For a ring equivalence f, ker f equals the bottom ideal, i.e., ker f = ⊥.

Русский

Для кольцевого эквивалента f ядро равно нижнему идеалу: ker f = ⊥.

LaTeX

$$$\\ker f = \\{0\\}$$$

Lean4

theorem ker_coe_toRingHom : ker (f : R →+* S) = ker f :=
  rfl

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

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

Разделы

Аффилиация

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