linearIndependent_subsingleton_iff

English

If M is subsingleton and R is nontrivial, LinearIndependent R f for a function f: ι → M is equivalent to IsEmpty ι.

Русский

Если M — пододин, R ненулевой, то LinearIndependent R f эквивалентно IsEmpty ι.

LaTeX

$$$[\\text{Nontrivial }R] [\\text{Subsingleton }M](f): \\operatorname{LinearIndependent}(R,f) \\iff \\operatorname{IsEmpty} ι$$$

Lean4

@[simp]
theorem linearIndependent_subsingleton_iff [Nontrivial R] [Subsingleton M] (f : ι → M) :
    LinearIndependent R f ↔ IsEmpty ι := by rw [Subsingleton.elim f 0, linearIndependent_zero_iff]

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