le_ker_iff_comp_subtype_eq_zero — Mathlib

English

For a submodule N of M and a semilinear map f, N is contained in ker f if and only if the composed map f ∘ N.subtype is zero.

Русский

Для подпмодуля N ⊆ M и пол линейного отображения f, N ⊆ ker f тогда и только тогда, когда композиция f с включением N в M равна нулю.

LaTeX

$$$N \leq \ker f \iff f \circ N.subtype = 0$$$

Lean4

theorem le_ker_iff_comp_subtype_eq_zero {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} : N ≤ ker f ↔ f ∘ₛₗ N.subtype = 0 := by
  rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]; rfl

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