English
Definition of an equivalence between the family of independent vectors of length n+1 and the pair described above.
Русский
Определение эквивалентности между независимой совокупностью векторов длины n+1 и указанной выше парой.
LaTeX
$$def equiv_linearIndependent (n : ℕ) : { s : Fin (n + 1) → V // LinearIndependent K s } ≃ Σ s : { s : Fin n → V // LinearIndependent K s }, ((Submodule.span K (Set.range (s : Fin n → V)))ᶜ : Set V)$$
Lean4
/-- Equivalence between `k + 1` vectors of length `n` and `k` vectors of length `n` along with a
vector in the complement of their span.
-/
def equiv_linearIndependent (n : ℕ) :
{ s : Fin (n + 1) → V // LinearIndependent K s } ≃
Σ s : { s : Fin n → V // LinearIndependent K s }, ((Submodule.span K (Set.range (s : Fin n → V)))ᶜ : Set V)
where
toFun
s :=
⟨⟨Fin.tail s.val, (linearIndependent_fin_succ.mp s.property).left⟩,
⟨s.val 0, (linearIndependent_fin_succ.mp s.property).right⟩⟩
invFun s := ⟨Fin.cons s.2.val s.1.val, linearIndependent_fin_cons.mpr ⟨s.1.property, s.2.property⟩⟩
left_inv _ := by simp only [Fin.cons_self_tail, Subtype.coe_eta]
right_inv := fun ⟨_, _⟩ => by
simp only [Fin.cons_zero, Subtype.coe_eta, Sigma.mk.inj_iff, Fin.tail_cons, heq_eq_eq, and_self]
