Similarity_Mapping_is_Linear_Operator
Provedlinear-algebralinear-operatorsproofwikisimilarity
Let be a vector space over a field . Let . Then the mapping defined by is a linear operator on . If then is an automorphism of , and The linear operators , where , are called '''similarities of '''.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Similarity_Mapping_is_Linear_Operator {K : Type _} [Field K] {V : Type _} [AddCommGroup V] [Module K V] (beta : K) : ∃ (phi : V →ₗ[K] V), forall x, phi x = beta • x := by sorrySource