ker_eq_bot — Mathlib

English

For a semilinear map f, ker f = ⊥ if and only if f is injective.

Русский

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

LaTeX

$$$\ker f = \perp \iff \text{Injective } f$$$

Lean4

theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f := by
  simpa [disjoint_iff_inf_le] using disjoint_ker' (f := f) (p := ⊤)

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