mapMatrix — Mathlib

English

The mapMatrix of a linear equivalence equals the mapMatrix of its inverse: f.mapMatrix.symm = (f.symm.mapMatrix).

Русский

Картограмма отображения матрицы равна отображению обратного отображения: f.mapMatrix.symm = (f.symm.mapMatrix).

LaTeX

$$$f.mapMatrix.symm = (f.symm.mapMatrix)$$$

Lean4

/-- The `LinearEquiv` between spaces of matrices induced by a `LinearEquiv` between their
coefficients. This is `Matrix.map` as a `LinearEquiv`. -/
@[simps apply]
def mapMatrix (f : α ≃ₛₗ[σᵣₛ] β) : Matrix m n α ≃ₛₗ[σᵣₛ] Matrix m n β :=
  { f.toEquiv.mapMatrix,
    f.toLinearMap.mapMatrix with
    toFun := fun M => M.map f
    invFun := fun M => M.map f.symm }

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