mul_nonsing_inv_cancel_left

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

For any B, A (A^{-1} B) = B when det(A) is a unit.

Русский

Для любого B выполняется A (A^{-1} B) = B, если det(A) — единица.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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