English
Let f: M → N be linear. If b, b' are bases of M and c, c' bases of N, then the matrix equation expressing the action of f under the bases b and c' is: [f]_{b,c'} · [b,b'] = [f]_{b,c'}. Equivalently, c.toMatrix c' · f.toMatrix(b',c') · b'.toMatrix b = f.toMatrix(b,c).
Русский
Пусть f: M → N — линейное. Пусть b, b' — базы M, c, c' — базы N. Тогда матричное представление f в базисах b и c' выражается как: [f]_{b,c'} · [b,b'] = [f]_{b,c'}. Эквивалентно, c.toMatrix c' · LinearMap.toMatrix b' c' f · b'.toMatrix b = LinearMap.toMatrix b c f.
LaTeX
$$$\text{ToMatrix}_{c,c'}(f) \cdot \text{ToMatrix}_{b',c'}(f) \cdot \text{ToMatrix}_{b',b} = \text{ToMatrix}_{b,c}(f)$$$
Lean4
theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix [Fintype κ'] [DecidableEq ι] [DecidableEq ι'] :
c.toMatrix c' * LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c f :=
by
cases nonempty_fintype κ
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]
