English
The linear map corresponding to a 2×2 matrix with respect to the FinTwoProd basis decomposes as the product of two coordinate maps, each encoding one row of the matrix.
Русский
Линейное отображение, задаваемое матрицей 2×2 в базисе FinTwoProd, раскладывается как произведение двух координатных отображений, каждая из которых кодирует одну строку матрицы.
LaTeX
$$$\text{toLin}_{v}(A) = (a\cdot \text{fst}_v + b\cdot \text{snd}_v) \; \text{prod} \; (c\cdot \text{fst}_v + d\cdot \text{snd}_v).$$$
Lean4
@[simp]
theorem toLin_finTwoProd_apply (a b c d : R) (x : R × R) :
Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x =
(a * x.fst + b * x.snd, c * x.fst + d * x.snd) :=
by simp [Matrix.toLin_apply, Matrix.mulVec, dotProduct]
