mapMatrix_symm — Mathlib

English

The inverse of the matrix-coefficient equivalence is induced by the inverse equivalence on coefficients.

Русский

Обратное к отображению матриц, получаемому из эквивалентности коэффициентов, задаётся через симметрическую эквивалентность коэффициентов.

LaTeX

$$$f.\\mathrm{mapMatrix}.\\mathrm{symm} = (f.\\mathrm{symm}.mapMatrix)$$$

Lean4

@[simp]
theorem mapMatrix_symm (f : α ≃ β) : f.mapMatrix.symm = (f.symm.mapMatrix : Matrix m n β ≃ _) :=
  rfl

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