vecMul_injective_of_invertible

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

← MathLib Explorer

English

For invertible A, vecMul is injective.

Русский

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

LaTeX

$$Injective A.vecMul$$

Lean4

theorem vecMul_injective_of_invertible (A : Matrix m m K) [Invertible A] : Function.Injective A.vecMul :=
  vecMul_injective_iff_isUnit.2 <| isUnit_of_invertible A

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

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

Разделы

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

Аффилиация

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