mapMatrix_symm

Mathlib.Data.Matrix.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.mapMatrix_symm

English

Composition commutes with mapMatrix: mapMatrix of the composed equivalence equals the composition of mapMatrices.

Русский

Сложение совпадает с mapMatrix: mapMatrix(f.trans g) = mapMatrix(f) . mapMatrix(g).

LaTeX

$$$f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru