|
chinese_remainder: THEORY
% The Chinese Remainder Theorem
% Author(s): Anthony Narkawicz
%
% Date: March 2012
BEGIN
IMPORTING ints@gcd,reals@product_nat
N: VAR posnat
m1,m2: VAR posnat
a1,a2: VAR nat
chinese_remainder_base : LEMMA
rel_prime(m1,m2) IMPLIES
EXISTS (k:below(m1*m2)): mod(a1,m1)=mod(k,m1) AND mod(a2,m2) = mod(k,m2)
mseq : VAR [nat->posnat]
aseq : VAR [nat->nat]
chinese_remainder : LEMMA
(FORALL (i,j:below(N)): i/=j IMPLIES rel_prime(mseq(i),mseq(j)))
IMPLIES
(EXISTS (k:nat): FORALL (i:below(N)): mod(aseq(i),mseq(i)) = mod(k,mseq(i)))
END chinese_remainder
¤ Dauer der Verarbeitung: 0.0 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.
|
