linearIndepOn_empty

Mathlib.LinearAlgebra.LinearIndependent.Defs

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

English

The independence on an empty index set is true: LinearIndepOn R v ∅.

Русский

Независимость на пустом множестве индексов верна: LinearIndepOn R v ∅.

LaTeX

$$$\\operatorname{linearIndepOnEmpty} :\\; \\operatorname{LinearIndepOn} R v \\emptyset$$$

Lean4

@[simp]
theorem linearIndepOn_empty : LinearIndepOn R v ∅ :=
  linearIndependent_empty_type ..

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

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

Разделы

Аффилиация

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