coe_basisOfLinearIndependentOfCardEqFinrank

English

If ι is a finite index set and b : ι → V is linearly independent with card ι = finrank K V, then the basis constructed from b is exactly b.

Русский

Если индексы ι конечны и b:ι → V линейно независимы при |ι| = finrank_K V, то созданная из b база совпадает с b.

LaTeX

$$$\\bigl(\\text{basisOfLinearIndependentOfCardEqFinrank }\\; \\text{lin_ind} \\; \\text{card_eq}\\bigr)$ коe равна $b$ на всех индексов: $\\forall i, \\; \\bigl(\\text{basisOfLinearIndependentOfCardEqFinrank }\\; lin\_ind\\; card\_eq\\bigr)(i) = b(i).$$$

Lean4

@[simp]
theorem coe_basisOfLinearIndependentOfCardEqFinrank {ι : Type*} [Nonempty ι] [Fintype ι] {b : ι → V}
    (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
    ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b :=
  Basis.coe_mk _ _

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