id_singleton

Mathlib.LinearAlgebra.LinearIndependent.Basic

URI: https://scilib.ai/kg/mathlib#LinearIndepOn.id_singleton

English

If x ≠ 0, then {x} is linearly independent.

Русский

Если x ≠ 0, то множество {x} линейно независимо.

LaTeX

$$$x \\neq 0 \\Rightarrow \\text{LinearIndepOn } R\\ id \\{x\\}$$$

Lean4

theorem id_singleton {x : M} (hx : x ≠ 0) : LinearIndepOn R id { x } :=
  linearIndependent_unique Subtype.val hx

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

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

Разделы

Аффилиация

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