right_inv_eq_left_inv

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If B A = 1 and C A = 1, then B = C.

Русский

Если B A = 1 и C A = 1, то B = C.

LaTeX

$$Theorem: If B A = 1 and C A = 1, then B = C.$$

Lean4

/-- The right inverse of matrix A equals the left inverse of A when they exist. -/
theorem right_inv_eq_left_inv (h : A * B = 1) (g : C * A = 1) : B = C := by
  rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]

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

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

Разделы

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

Аффилиация

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