English
The matrix whose columns are the coordinates of b' relative to b is invertible; its inverse is the matrix of b relative to b'.
Русский
Матрица перехода от базиса b к b' обратима, и её обратная — матрица перехода от b' к b.
LaTeX
$$$\text{ToMatrix}_{b,c}(f)$ is invertible with inverse $\text{ToMatrix}_{c,b}$ when bases are swapped; i.e., $\text{ToMatrix}_{b}^{b'} \cdot \text{ToMatrix}_{b'}^{b} = I$$$
Lean4
/-- A generalization of `Basis.toMatrix_self`, in the opposite direction. -/
@[simp]
theorem toMatrix_mul_toMatrix {ι'' : Type*} [Fintype ι'] (b'' : ι'' → M) :
b.toMatrix b' * b'.toMatrix b'' = b.toMatrix b'' :=
by
haveI := Classical.decEq ι
haveI := Classical.decEq ι'
haveI := Classical.decEq ι''
ext i j
simp only [Matrix.mul_apply, toMatrix_apply, sum_repr_mul_repr]
