Stretching_Contraction_are_Linear
Provedlinear-algebralinear-operatorsproofwikisimilarity
Let be a similarity of . Then is the same as the rotation of the plane about the origin one half turn. If , then is called a '''stretching''', and if , is called a '''contraction'''. If , then is a stretching or contraction followed by a rotation one half turn. It is also the same as a rotation one half turn followed by a stretching or contraction.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Stretching_Contraction_are_Linear (beta : ℝ) : ∃ (phi : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ)), forall x, phi x = beta • x := by sorry
Source