ker_compLeft — Mathlib

English

Alternative presentation of ker_compLeft as a product-of-kernels description.

Русский

Альтернативное представление ядра ker_compLeft через произведение ядер.

LaTeX

$$$$\\ker(f\\circ_{Left}I) = \\pi Set.univ (\\ker f).$$$$

Lean4

theorem ker_compLeft [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (I : Type*) :
    LinearMap.ker (f.compLeft I) = Submodule.pi (Set.univ : Set I) (fun _ => LinearMap.ker f) :=
  Submodule.ext fun _ => ⟨fun (hx : _ = _) i _ => congr_fun hx i, fun hx => funext fun i => hx i trivial⟩

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