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