injective_iff_ker_eq_bot

Mathlib.RingTheory.Ideal.Maps

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

← MathLib Explorer

English

A ring homomorphism f is injective if and only if ker f = ⊥.

Русский

Гомоморфизм f инъективен тогда и только тогда, когда ker f = ⊥.

LaTeX

$$$\\operatorname{Injective}(f) \\iff \\ker f = \\{0\\}$$$

Lean4

theorem injective_iff_ker_eq_bot : Function.Injective f ↔ ker f = ⊥ :=
  by
  rw [SetLike.ext'_iff, ker_eq, Set.ext_iff]
  exact injective_iff_map_eq_zero' f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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