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]