ker_prod — Mathlib

English

The kernel of the product map f.prod g equals ker f ∩ ker g.

Русский

Ядро произведения отображений f.prod g равно пересечению ядер f и g.

LaTeX

$$@[simp] theorem ker_prod (f : M1 →L[R] M2) (g : M1 →L[R] M3) : ker (f.prod g) = ker f ⊓ ker g$$

Lean4

@[simp]
theorem ker_prod (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) : ker (f.prod g) = ker f ⊓ ker g :=
  LinearMap.ker_prod (f : M₁ →ₗ[R] M₂) (g : M₁ →ₗ[R] M₃)

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