Linear_Transformation_of_Submodule
Provedlinear-algebralinear-transformationsmodulesproofwiki
Let and be -modules. Let be a linear transformation. Then If is a submodule of , is a submodule of If is a submodule of , is a submodule of The codomain of is a submodule of The kernel of is a submodule of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Linear_Transformation_of_Submodule {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (phi : M →ₗ[R] N) (H : Submodule R M) : ∃ (K : Submodule R N), (K : Set N) = phi '' (H : Set M) := by sorrySource