toMatrix'_symm — Mathlib

English

A reindexed matrix induces a mulVecLin map equal to the conjugation by suitable LinearEquiv on both sides.

Русский

Переиндексированная матрица задаёт mulVecLin, равный сопряжению подходящими линейными эквивалентностями слева и справа.

LaTeX

$$mulVecLin_reindex [Fintype n] [Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) :\n (reindex e₁ e₂ M).mulVecLin =\n ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)$$

Lean4

@[simp]
theorem toMatrix'_symm : (LinearMap.toMatrix'.symm : Matrix m n R ≃ₗ[R] _) = Matrix.toLin' :=
  rfl

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