linearIndepOn_zero_iff

Mathlib.LinearAlgebra.LinearIndependent.Defs

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

English

Equivalently, under simplifications, LI 0 is equivalent to ι being empty.

Русский

Эквивалентно, в упрощённой форме, LI 0 эквивалентно пустоте индексов ι.

LaTeX

$$$\\operatorname{linearIndependentZero}\\ \\text{iff } ι=\\varnothing$$$

Lean4

@[simp]
theorem linearIndepOn_zero_iff [Nontrivial R] : LinearIndepOn R (0 : ι → M) s ↔ s = ∅ :=
  linearIndependent_zero_iff.trans isEmpty_coe_sort

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

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

Разделы

Аффилиация

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