ker_eq

Mathlib.RingTheory.Ideal.Maps

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

English

Let f: R → S be a ring homomorphism. Then ker f equals the preimage of {0} under f, i.e., ker f = f^{-1}({0}).

Русский

Пусть f: R → S — гомоморфизм колец. Тогда ker f совпадает с предобразом множества {0} под действием f, т.е. ker f = f^{-1}({0}).

LaTeX

$$$\\ker f = f^{-1}(\\{0\\})$$$

Lean4

theorem ker_eq : (ker f : Set R) = Set.preimage f {0} :=
  rfl

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

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

Разделы

Аффилиация

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