Linear_Operator_on_the_Plane
Provedlinear-algebralinear-operatorsplaneproofwiki
Let be a linear operator on the real vector space of two dimensions . Then is completely determined by an ordered tuple of real numbers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Linear_Operator_on_the_Plane (phi : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ)) : ∃ (a b c d : ℝ), forall (x : Fin 2 → ℝ), phi x 0 = a * x 0 + b * x 1 ∧ phi x 1 = c * x 0 + d * x 1 := by sorry
Source