ker_prodMap — Mathlib

English

The kernel of the product map f.prodMap g is the product of the kernels: ker(f.prodMap g) = ker f × ker g.

Русский

Ядро отображения f.prodMap g равно произведению ядер: ker(f.prodMap g) = ker f × ker g.

LaTeX

$$$ \\ker (\\text{LinearMap.prodMap } f g) = \\ker f \\;\\text{.prod}\\; \\ker g.$$$

Lean4

theorem ker_prodMap (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) : ker (LinearMap.prodMap f g) = Submodule.prod (ker f) (ker g) :=
  by
  dsimp only [ker]
  rw [← prodMap_comap_prod, Submodule.prod_bot]

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