inv_mul_cancel_left_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

Let A be invertible. Then A^{-1} (A B) = B for any B.

Русский

Пусть A обратима. Тогда A^{-1} (A B) = B для любой матрицы B.

LaTeX

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

Lean4

@[simp]
theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B :=
  nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A)

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

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

Разделы

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

Аффилиация

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