mul_right_inj_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

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

Русский

При обратимой $A$ отображение $x \mapsto A x$ инъективно.

LaTeX

$$Injective (A x) ↦ x$$

Lean4

theorem mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x = A * y ↔ x = y :=
  (mul_right_injective_of_invertible A).eq_iff

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

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

Разделы

Аффилиация

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