English
When both domain and codomain are equipped with the standard basis Pi.basisFun R n and Pi.basisFun R n, the matrix-to-linear-map construction coincides with the canonical matrix construction, i.e., LinearMap.toMatrix for standard bases equals LinearMap.toMatrix'.
Русский
Когда как область, так и кодобласть имеют стандартный базис Pi.basisFun R n, построение матрицы линейного отображения совпадает с каноническим представлением матрицы: LinearMap.toMatrix для стандартных базисов равен LinearMap.toMatrix'.
LaTeX
$$$\\text{toMatrix}_{\\mathrm{std},\\mathrm{std}} = \\text{toMatrix}'.$$$
Lean4
/-- `LinearMap.toMatrix'` is a particular case of `LinearMap.toMatrix`, for the standard basis
`Pi.basisFun R n`. -/
@[simp]
theorem toMatrix_eq_toMatrix' : LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix' :=
rfl
