mapMatrix_symm — Mathlib

English

The inverse of the matrix map induced by an additive equivalence equals the matrix map induced by the inverse additive equivalence.

Русский

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

LaTeX

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

Lean4

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

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