mul_inv_eq_iff_eq_mul_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

For invertible A, B A^{-1} = C if and only if B = C A.

Русский

Для обратимой A: B A^{-1} = C эквивалентно B = C A.

LaTeX

$$$B A^{-1}=C \iff B=C A$$$

Lean4

theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] : B * A⁻¹ = C ↔ B = C * A :=
  ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible], fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩

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

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

Разделы

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

Аффилиация

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