nonsing_inv_mul_cancel_right

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If A is invertible, then A A^{-1} = I.

Русский

Если A обратима, то A A^{-1} = I.

LaTeX

$$$A A^{-1} = I$ for invertible A$$

Lean4

@[simp]
theorem nonsing_inv_mul_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B := by
  simp [Matrix.mul_assoc, nonsing_inv_mul A h]

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

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

Разделы

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

Аффилиация

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