basisOfPiSpaceOfLinearIndependent

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

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

Lean4

/-- In a vector space `ι → K`, a linear independent family indexed by `ι` is a basis. -/
noncomputable def basisOfPiSpaceOfLinearIndependent {ι : Type*} [Fintype ι] [Decidable (Nonempty ι)] {b : ι → (ι → K)}
    (hb : LinearIndependent K b) : Basis ι K (ι → K) :=
  if hι : Nonempty ι then basisOfLinearIndependentOfCardEqFinrank hb (Module.finrank_fintype_fun_eq_card K).symm
  else
    have : IsEmpty ι := not_nonempty_iff.mp hι
    Basis.empty _

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

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

Разделы

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

Аффилиация

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