compAddEquiv_symm_apply

Mathlib.Data.Matrix.Composition

URI: https://scilib.ai/kg/mathlib#Matrix.compAddEquiv_symm_apply

English

The inverse of compAddEquiv on M equals the inverse under comp on M.

Русский

Обратное от compAddEquiv на M равно обратному от comp на M.

LaTeX

$$$ (\mathrm{compAddEquiv})^{-1}(M) = (\mathrm{comp})^{-1}(M) $$$

Lean4

@[simp]
theorem compAddEquiv_symm_apply (M : Matrix (I × K) (J × L) R) :
    (compAddEquiv I J K L R).symm M = (comp I J K L R).symm M :=
  rfl

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

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

Разделы

Аффилиация

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