% @(#)$Id: PreVectorSpace.lsl,v 1.3 1997/06/05 03:10:53 leavens Exp $
PreVectorSpace(T): trait

  assumes RingWithUnit, Abelian(* for \circ)

  includes AbelianGroup(Vec[T] for T, + for \circ,
                        0 for unit, - __ for \inv),
           DistributiveRingAction(T for M, Vec[T] for T)

  implies

    AC(+ for \circ, Vec[T] for T), Idempotent(- __, Vec[T])

    \forall u,v,w: Vec[T], a, b: T

      % the usual axioms, apart from the abelian group axioms
      a * (u + v) == (a * u) + (a * v);
      (a + b) * u == (a * u) + (b * u);
      (a * b) * u == a * (b * u);
      1 * u == u;
      u - v == u + (- v);

      % some standard theorems
      (u + v = u + w) => v = w;
      0 * u == 0:Vec[T];
      -(a * u) == (-a) * u;
      -(a * u) == a * (-u);
      (-a) * (-u) == a * u;
      (a \neq 0 /\ a * u = a * v) => u = v;

    converts
      0: -> Vec[T],
      __+__: Vec[T], Vec[T] -> Vec[T],
      __*__: T, Vec[T] -> Vec[T],
      - __: Vec[T] -> Vec[T],
      __ - __: Vec[T], Vec[T] -> Vec[T]

[Index]

HTML generated using lcpp2html.