ker_coprod_of_disjoint_range — Mathlib

English

If the ranges of two maps are disjoint, then the kernel of their coprod is the product of the kernels: ker(f1.coprod f2) = ker f1 .prod ker f2.

Русский

Если образы двух отображений дизъюнкты, то ядро их coprod равно произведению ядер: ker(f1.coprod f2) = ker f1 .prod ker f2.

LaTeX

$$$$ \ker(f_1.coprod f_2) = \ker f_1 \;\mathrm{prod}\; \ker f_2 \\text{when } \mathrm{range}(f_1) \perp \mathrm{range}(f_2) $$$$

Lean4

theorem ker_coprod_of_disjoint_range {f₁ : M₁ →L[R] M} {f₂ : M₂ →L[R] M} (hf : Disjoint (range f₁) (range f₂)) :
    LinearMap.ker (f₁.coprod f₂) = (LinearMap.ker f₁).prod (LinearMap.ker f₂) :=
  LinearMap.ker_coprod_of_disjoint_range f₁.toLinearMap f₂.toLinearMap hf

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