linearIndependent_equiv — Mathlib

English

The linear independence of a family is preserved under composition with an equivalence of index types.

Русский

Линейная независимость семейства сохраняется при композиции с эквиваленцией индексов.

LaTeX

$$$\\\\mathrm{linearIndependent}_{R} (f \\circ e) \\\\iff \\\\mathrm{linearIndependent}_{R} f,$ для эквививалентности $e : ι \\simeq ι'$.$$

Lean4

theorem linearIndependent_equiv (e : ι ≃ ι') {f : ι' → M} : LinearIndependent R (f ∘ e) ↔ LinearIndependent R f :=
  ⟨fun h ↦ comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective, fun h ↦ h.comp _ e.injective⟩

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