inv_mulVec_eq_vec

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If u = A v for an invertible A, then A^{-1} u = v.

Русский

Если $u = A v$ для обратимой $A$, то $A^{-1} u = v$.

LaTeX

$$$u = A\,v \implies A^{-1}u = v$$$

Lean4

theorem inv_mulVec_eq_vec {A : Matrix n n α} [Invertible A] {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v := by
  rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]

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

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

Разделы

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

Аффилиация

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