Require Import Field_theory.

Section Vector_Spaces.
  Variable (R:Type)
    (rO:R) (rI:R)
    (radd rmul rsub : R → R → R)
    (ropp : R → R)
    (rdiv : R → R → R)
    (rinv : R → R)
    (req : R → R → Prop)
  .
  Variable Rfield : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
  Variable (V:Type) (vO:V).
  Variable vadd : V→V→V.
  Variable smul : R→V→V.

  Record vector_space : Type := {
    vadd_comm := ∀ x y, vadd x y = vadd y x;
    vadd_assoc := ∀ x y z, vadd (vadd x y) z = vadd x (vadd y z);
    vadd_identity := ∀ x, vadd vO x = x;
    vadd_inverse := ∀ x, ∃ y, vadd x y = vO;
  
    smul_distr_vadd := ∀ a x y, smul a (vadd x y) = vadd (smul a x) (smul a y);
    smul_distr_radd := ∀ a b x, smul (radd a b) x = vadd (smul a x) (smul b x);
    smul_compat_rmul := ∀ a b x, smul a (smul b x) = smul (rmul a b) x;
    smul_identity := ∀ x, smul rI x = x
  }.

  Fixpoint finite_sum (n:nat) (v:nat→V) {struct n} := match n with
    | 0 ⇒ vO
    | S i ⇒ vadd (v n) (finite_sum i v)
  end.

  Record Basis (I:Type) (Xi:I→V) : Prop := {
    basis_spanning : ∀ x:V, ∃ n, ∃ vn : nat → I,
      x = finite_sum n (fun n ⇒ Xi (vn n));
    basis_linear_independence : ∀ n (vn : nat→I) (an : nat→R),
      (∀ i j , i≤n → j≤n → vn i = vn j → i=j) →
      finite_sum n (fun m ⇒ Xi (vn m)) = vO →
      ∀ i, i≤n → an i = rO
  }.

End Vector_Spaces.