Linear_Transformation_from_Ordered_Basis_less_Kernel
Provedkernellinear-algebralinear-transformationsmodulesproofwiki
Let and be unitary -modules. Let be a non-zero linear transformation. Let be -dimensional. Let be any ordered basis of such that is the basis of the kernel of . Then is an ordered basis of the image of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Linear_Transformation_from_Ordered_Basis_less_Kernel {R : Type _} [CommRing R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (phi : M →ₗ[R] N) : LinearMap.range phi = Submodule.map phi ⊤ := by sorrySource