ker_comp — Mathlib

English

Same principle as above: the kernel of the composed linear map with a linear equivalence equals the kernel of the original map.

Русский

Тот же принцип: ядро композиции линейного отображения с линейным эквивалентом равно ядру исходного отображения.

LaTeX

$$$\ker((e''\circ l)) = \ker l$$$

Lean4

@[simp]
theorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) :
    LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) = LinearMap.ker l :=
  LinearMap.ker_comp_of_ker_eq_bot _ e''.ker

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