division_ring_def.pvs

%------------------------------------------------------------------------------
% Division rings definition file
%
%     Author: Rick Butler
%             David Lester, Manchester University & NIA
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

division_ring_def[T:Type+,+,*:[T,T->T],zero,one:T]: THEORY

BEGIN

   IMPORTING ring_def, ring_with_one_def[T,+,*,zero,one], group_def

   division_ring?(S:set[T]):bool = ring_with_one?(S) AND
                                   group?[T,*,one](remove(zero,S))

END division_ring_def