ker_smul' — Mathlib

English

For a linear map f and a scalar a, the kernel of a • f is the infimum over all a ≠ 0 of ker f.

Русский

Для линейного отображения f и скаляра a ядро(a·f) равно пересечению (наименьшее) всех ker f по всем a≠0.

LaTeX

$$$\ker(a\cdot f) = \bigwedge_{a \neq 0} \ker f$$

Lean4

theorem ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f :=
  Submodule.comap_smul' f _ a

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