toMatrix_smulBasis_right — Mathlib

English

Analogous generalization for right action: twisting the codomain basis by g yields the corresponding transformation of the matrix of f.

Русский

Аналогичное обобщение для правого действия: изменение кодобазы через g приводит к соответствующему преобразованию матрицы f.

LaTeX

$$$\\forall g, f:\\; \\text{toMatrix } v_1 (g \\cdot v_2) f = \\text{toMatrix } v_1 v_2 (\\text{DistribMulAction.toLinearMap } R M_2 g^{-1} \\circ f).$$$

Lean4

theorem toMatrix_smulBasis_right {G} [Group G] [DistribMulAction G M₂] [SMulCommClass G R M₂] (g : G)
    (f : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix v₁ (g • v₂) f = LinearMap.toMatrix v₁ v₂ (DistribMulAction.toLinearMap _ _ g⁻¹ ∘ₗ f) := by rfl

Похожие утверждения