inv_reindex

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

A direct variant of inv_reindex: inv(reindex e1 e2 A) equals reindex e2 e1 of the inverse of A.

Русский

Прямой вариант inv_reindex: inv(reindex e1 e2 A) = reindex e2 e1 (A^{-1}).

LaTeX

$$inv(reindex e1 e2 A) = reindex e2 e1 (A^{-1})$$

Lean4

theorem inv_reindex (e₁ e₂ : n ≃ m) (A : Matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ A⁻¹ :=
  inv_submatrix_equiv A e₁.symm e₂.symm

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

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

Разделы

Аффилиация

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