fact: Record R_vector_space : Type := { vadd_comm : forall x y, vadd x y = vadd y x; vadd_assoc : forall x y z, vadd (vadd x y) z = vadd x (vadd y z); vadd_identity : forall x, vadd vO x = x; vadd_inverse : forall x, {y | vadd x y = vO} ; smul_distr_vadd : forall a x y, smul a (vadd x y) = vadd (smul a x) (smul a y); smul_distr_radd : forall a b x, smul (a + b) x = vadd (smul a x) (smul b x); smul_compat_rmul : forall a b x, smul a (smul b x) = smul (a * b) x; smul_identity : forall x, smul R1 x = x; Nzero : forall x, N x = 0 -> x = vO; Nmul : forall lambda x, N (smul lambda x) = Rabs (lambda) * N x; Ntriang : forall x y, N (vadd x y) <= N x + N y; basis : forall (v : V), v = finite_sum dim (fun n => smul (p n v) (base n)) }.
imports: Reals