mul_inv_rev

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

The inverse of a product reverses factors: (A B)^{-1} = B^{-1} A^{-1}.

Русский

Обратная произведения меняет порядок факторов: (AB)^{-1} = B^{-1} A^{-1}.

LaTeX

$$(A B)^{-1} = B^{-1} A^{-1}$$

Lean4

theorem mul_inv_rev (A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹ :=
  by
  simp only [inv_def]
  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib, Ring.mul_inverse_rev]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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