linearIndependent_empty

Mathlib.LinearAlgebra.LinearIndependent.Defs

URI: https://scilib.ai/kg/mathlib#linearIndependent_empty

English

If ι is empty, then any v is linearly independent.

Русский

Если ι пуст, то любой v линейно независим.

LaTeX

$$$[IsEmpty ι] :\\; \\operatorname{LinearIndependent}(R,v)$$$

Lean4

theorem linearIndependent_empty : LinearIndependent R (fun x => x : (∅ : Set M) → M) :=
  linearIndependent_empty_type

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

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

Разделы

Аффилиация

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