English
For a group G acting on M1 and a linear map f, the matrix of f with respect to the twisted left basis g•v1 equals the matrix of f composed with the corresponding linear action.
Русский
Для группы G действующей на M1 и отображения f, матрица f относительно левого базиса g•v1 равна матрице f, композиции с соответствующим линейным действием.
LaTeX
$$$\\text{toMatrix } (g \\cdot v_1) v_2 f = \\text{toMatrix } v_1 v_2 (f \\circ (\\text{DistribMulAction.toLinearMap } R M_1 g)).$$$
Lean4
theorem toMatrix_mulVec_repr (f : M₁ →ₗ[R] M₂) (x : M₁) : LinearMap.toMatrix v₁ v₂ f *ᵥ v₁.repr x = v₂.repr (f x) :=
by
ext i
rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
congr
exact v₁.equivFun.symm_apply_apply x
