ker_restrict — Mathlib

English

For f: M →ₗ[R] M1 and p ⊆ M, ker (f.restrict p) = (ker f).comap p.subtype.

Русский

Для f: M →ₗ[R] M1 и p ⊆ M, ker (f.restrict p) = (ker f).comap p.subtype.

LaTeX

$$ker (f.restrict hf) = (ker f).comap p.subtype$$

Lean4

theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} {f : M →ₗ[R] M₁}
    (hf : ∀ x : M, x ∈ p → f x ∈ q) : ker (f.restrict hf) = (ker f).comap p.subtype := by
  rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

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