一次独立・基底・次元

一次独立性は LinearIndependent K v で表します． ここで v : ι → V は添字集合 ι で添字づけられたベクトルの族です． 基底は Basis ι K V で，添字集合 ι を持つ K 上の V の基底です．

#check LinearIndependent
#check Module.Basis
#check Module.rank
#check Module.finrank

section Dimension

variable {K : Type*} [Field K]

example : Module.finrank K (Fin 3 → K) = 3 := by
  simp

example : Module.finrank K K = 1 := by
  simp

end Dimension

Module.rank は基数値の次元です． FiniteDimensional.finrank は自然数値の次元で，無限次元の場合は慣習的に 0 になります． 有限次元と分かっている状況では finrank が計算しやすいことが多いです．