Addition_of_Linear_Transformations
Provedlinear-algebralinear-transformationsproofwiki
Let and be -modules. Let and be linear transformations. Let be the operation on induced by as defined in Induced Structure. Then is a linear transformation.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Addition_of_Linear_Transformations {R : Type _} [Ring R] {M N : Type _} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (phi psi : M →ₗ[R] N) : ∃ (sigma : M →ₗ[R] N), forall x, sigma x = phi x + psi x := by sorrySource