|
%------------------------------------------------------------------------------
% Rings in which the nonzero elements are closed under *
%
% This is defined so that inheriting properties of nz_T work
% correctly in field, where we rejoin properties from divison rings
% and intgral domains.
%
%
% 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
%------------------------------------------------------------------------------
ring_nz_closed[T:Type+,+,*:[T,T->T],zero:T]: THEORY
BEGIN
ASSUMING IMPORTING ring_def[T,+,*,zero],
ring_nz_closed_def[T,+,*,zero]
fullset_is_ring_nz_closed: ASSUMPTION ring_nz_closed?(fullset[T])
ENDASSUMING
IMPORTING ring_nz_closed_def[T,+,*,zero],
ring[T,+,*,zero], monoid, operator_defs_more[T]
ring_nz_closed: TYPE+ = (ring_nz_closed?) CONTAINING fullset[T]
R: VAR ring_nz_closed
x,y: VAR T
nzx,nzy: VAR nz_T
ring_nz_closed_is : LEMMA ring_nz_closed?(R)
ring_nz_closed_is_ring : JUDGEMENT ring_nz_closed SUBTYPE_OF ring
nz_T_times_nz_T_is_nz_T : JUDGEMENT *(nzx, nzy) HAS_TYPE nz_T
negate_nz_T_is_nz_T : JUDGEMENT inv(nzx) HAS_TYPE nz_T
times_is_zero : LEMMA x * y = zero IFF x = zero OR y = zero
nz_T_times : LEMMA nzx * y = zero IFF y = zero
times_nz_T : LEMMA x * nzy = zero IFF x = zero
nz_T_times_nz_T_is_not_zero: LEMMA nzx * nzy /= zero
sq_nz_is_nz : JUDGEMENT sq(nzx) HAS_TYPE nz_T
sq_eq_zero : LEMMA sq(x) = zero IFF x = zero
END ring_nz_closed
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
