linearIndependent_zero_iff — Mathlib

English

For nontrivial R, LinearIndependent R (0 : ι → M) holds iff ι is empty.

Русский

Для ненулевого R линейная независимость нулевой карты эквивалентна тому, что ι пусто.

LaTeX

$$$[\\text{Nontrivial }R] :\\; \\operatorname{LinearIndependent}(R,0) \\iff \\operatorname{IsEmpty}\\ ι$$$

Lean4

@[simp]
theorem linearIndependent_zero_iff [Nontrivial R] : LinearIndependent R (0 : ι → M) ↔ IsEmpty ι :=
  ⟨fun h ↦ not_nonempty_iff.1 fun ⟨i⟩ ↦ (h.ne_zero i rfl).elim, fun _ ↦ linearIndependent_empty_type⟩

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