inv_eq_right_inv

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If A⁻¹ = B⁻¹ and det(A) is a unit, then A = B.

Русский

Если A⁻¹ = B⁻¹ и det(A) обратимо, то A = B.

LaTeX

$$$A^{-1}=B^{-1} \wedge IsUnit(\det A) \Rightarrow A=B.$$$

Lean4

/-- If matrix A is right invertible, then its inverse equals its right inverse. -/
theorem inv_eq_right_inv (h : A * B = 1) : A⁻¹ = B :=
  inv_eq_left_inv (mul_eq_one_comm.2 h)

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

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

Разделы

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

Аффилиация

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