ker_prod — Mathlib

English

Let f: M → M₂ and g: M → M₃ be linear maps. Then ker(prod f g) = ker f ∩ ker g, i.e. the kernel of the pair map is the intersection of the kernels.

Русский

Пусть f: M → M₂ и g: M → M₃ — линейные отображения. Тогда ker(prod f g) = ker f ∩ ker g, то есть ядро пары отображений равно пересечению их ядер.

LaTeX

$$$\\ker(\\mathrm{prod}(f,g)) = \\ker f \\cap \\ker g.$$$

Lean4

@[simp]
theorem ker_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ker (prod f g) = ker f ⊓ ker g := by
  rw [ker, ← prod_bot, comap_prod_prod]; rfl

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