mul_left_inj_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

English

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

Русский

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

LaTeX

$$x A = y A ⇒ x = y$$

Lean4

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

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

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

Разделы

Аффилиация

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