-rw-r--r-- 882 leangoppa-20230726/Goppadecoding/lineardependence.lean raw
import Mathlib.LinearAlgebra.FiniteDimensional

namespace Goppadecoding

section lemmas_lineardependence

variable {k: Type _} [Field k]
variable {V: Type _} [AddCommGroup V] [Module k V] [Module.Finite k V]

open FiniteDimensional Submodule

theorem card_family_le_finrank_space_if_linearIndependent {S: Type _} [Fintype S] {b: S → V}:
  LinearIndependent k b → Fintype.card S ≤ finrank k V := by
    intro independent
    calc 
      Fintype.card S = (Set.range b).finrank k := linearIndependent_iff_card_eq_finrank_span.mp independent
      _ ≤ finrank k V := by apply finrank_le

theorem dependency_if_finrank_space_lt_card_family {S: Type _} [Fintype S] {b: S → V}:
  finrank k V < Fintype.card S → ¬LinearIndependent k b := by
    contrapose
    simp only [not_not, not_lt]
    apply card_family_le_finrank_space_if_linearIndependent

end lemmas_lineardependence