Hi,
Yes, I think what you need for aks-16-18 is something like:
aks.16 $e |- ph -> A. a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R
) ) x. ( 2 logb N ) ) ) ) ) ( ( a gcd N ) = 1 /\ ( ( M + a ) ^ N )
= ( ( M ^ N ) + a ) ) $.
Or equivalently:
aks.16ALT $e |- ( ( ph /\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi `
R ) ) x. ( 2 logb N ) ) ) ) ) -> ( a gcd N ) = 1 ) $.
aks.17ALT $e |- ( ( ph /\ a e. ( 1 ... ( |_ ` ( ( sqrt ` ( phi ` R
) ) x. ( 2 logb N ) ) ) ) ) -> ( ( M + a ) ^ N ) = ( ( M ^ N )
+ a ) ) $.
Using a set variable `a` there will allow you to switch easily to
the universal quantifier.
For aks.7, you'll want to have G = ( Z/nZ ` N ), and then G is your group (or actually, ring).
For aks,11 and aks.14, you can probably keep R in NN0, and use ( ( ZRHom ` G ) ` R ) to map it to the corresponding element of G = ( Z/nZ ` N ) (which is actually an equivalence class).
As far as the Galois Limit Field GF_oo is concerned, there are not theorems about it yet, so my guess is that we'll need to develop that theory first!
_
Thierry
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/834460ada90a2c25d144a5a9f37fbd32%40mail.eclipso.de.