mul_left_injective_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

If A is invertible, the map x ↦ x A is injective.

Русский

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

LaTeX

$$Injective (\lambda x, x A)$$

Lean4

theorem mul_left_injective_of_invertible [Invertible A] : Function.Injective (fun (x : Matrix m n α) => x * A) :=
  fun a x hax => by simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax

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

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

Разделы

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

Аффилиация

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