toMatrix_basis_equiv — Mathlib

English

Dual to the left action, if the codomain basis is twisted by a group element g, the matrix transforms accordingly by the inverse action.

Русский

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

LaTeX

$$$\\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

@[simp]
theorem toMatrix_basis_equiv [Fintype l] [DecidableEq l] (b : Basis l R M₁) (b' : Basis l R M₂) :
    LinearMap.toMatrix b' b (b'.equiv b (Equiv.refl l) : M₂ →ₗ[R] M₁) = 1 :=
  by
  ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

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