finsetBasisOfLinearIndependentOfCardEqFinrank

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

URI: https://scilib.ai/kg/mathlib#finsetBasisOfLinearIndependentOfCardEqFinrank

Lean4

/-- A linear independent finset of `finrank K V` vectors forms a basis. -/
@[simps! repr_apply]
noncomputable def finsetBasisOfLinearIndependentOfCardEqFinrank {s : Finset V} (hs : s.Nonempty)
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) : Basis s K V :=
  @basisOfLinearIndependentOfCardEqFinrank _ _ _ _ _ _ ⟨(⟨hs.choose, hs.choose_spec⟩ : s)⟩ _ _ lin_ind
    (_root_.trans (Fintype.card_coe _) card_eq)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru