linearIndependent_subsingleton_index_iff

English

For a subsingleton index, linear independence reduces to nonzero of the single coordinate.

Русский

Для индекса‑синглтона линейная независимость сводится к не нулю единственной координаты.

LaTeX

$$[simp] theorem linearIndependent_subsingleton_index_iff {ι} (f : ι → M) : LinearIndependent R f ↔ ∀ i, f i ≠ 0$$

Lean4

@[simp]
theorem linearIndependent_subsingleton_index_iff [Subsingleton ι] (f : ι → M) : LinearIndependent R f ↔ ∀ i, f i ≠ 0 :=
  by
  obtain (he | he) := isEmpty_or_nonempty ι
  · simp [linearIndependent_empty_type]
  obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩
  rw [linearIndependent_unique_iff]
  exact ⟨fun h i ↦ by rwa [Unique.eq_default i], fun h ↦ h _⟩

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