ker_eq_bot — Mathlib

English

For a ring homomorphism f, ker f = 0 if and only if f is injective.

Русский

Для отображения f ядро равно нулю тогда и только тогда, когда f инъективно.

LaTeX

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

Lean4

theorem ker_eq_bot : ker f = ⊥ ↔ Function.Injective f :=
  by
  fconstructor
  · intro h x y hxy
    simpa [h, rel_iff, mem_bot, sub_eq_zero] using show (ker f).ringCon x y from hxy
  · exact fun h ↦ eq_bot_iff.2 fun x hx => h hx

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