LinearIndepOn_iff_linearIndepOn_image_injOn

English

Equivalence of linear independence under unit-scale multipliers; LinearIndependent R (w • v) ↔ LinearIndependent R v for w: indices → units.

Русский

Эквивалентность независимости при множителях-единицах; LinearIndependent_R (w • v) ↔ LinearIndependent_R v для w: индексы→единицы.

LaTeX

$$$\text{LinearIndependent}_R(v) \iff \text{LinearIndependent}_R (w \cdot v)$ for w : ι → R^{×}$$

Lean4

theorem LinearIndepOn_iff_linearIndepOn_image_injOn [Nontrivial R] :
    LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ InjOn v s :=
  ⟨fun h ↦ ⟨h.id_image, h.injOn⟩, fun h ↦ (linearIndepOn_iff_image h.2).2 h.1⟩

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