mul_right_injective_of_inv

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If h: A B = 1, then the map x ↦ B x is injective.

Русский

Если $A B = 1$, то отображение $x \mapsto B x$ инъективно.

LaTeX

$$Injective (x \mapsto B x) given A B = 1$$

Lean4

theorem mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
    Function.Injective (fun x : Matrix m l α => B * x) := fun _ _ g => by
  simpa only [← Matrix.mul_assoc, Matrix.one_mul, h] using congr_arg (A * ·) g

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

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

Разделы

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

Аффилиация

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