ker_prod_ker_le_ker_coprod — Mathlib

English

Let f: M → M₃ and g: M₂ → M₃ be linear maps. Then (ker f) × (ker g) ⊆ ker(f.coprod g), since f(m) + g(n) = 0 when m ∈ ker f and n ∈ ker g.

Русский

Пусть f: M → M₃ и g: M₂ → M₃ — линейные отображения. Тогда (ker f) × (ker g) ⊆ ker(f.coprod g), поскольку f(m) + g(n) = 0 при m ∈ ker f и n ∈ ker g.

LaTeX

$$$(\\ker f) \\times (\\ker g) \\subseteq \\ker(f \\coprod g).$$$

Lean4

theorem ker_prod_ker_le_ker_coprod {M₂ : Type*} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type*} [AddCommMonoid M₃]
    [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : (ker f).prod (ker g) ≤ ker (f.coprod g) :=
  by
  rintro ⟨y, z⟩
  simp +contextual

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