Re: Re: [Metamath] Definition of product of polynomials.

['Meta Kunt' via Metamath]

Would you check if the following matches the definition of Claim 1 in 6.1?
I've tried, painstakingly, to match the definitions. A typo now would be horrific.
Reference: https://www3.nd.edu/~andyp/notes/AKS.pdf
1:: |- ( ph -> K e. Field )
2:: |- R = ( Poly1 ` K )
3:: |- B = ( Base ` K )
4:: |- X = ( var1 ` K )
5:: |- W = ( mulGrp ` R )
6:: |- M = ( mulGrp ` K )
7:: |- D = ( .g ` M )
8:: |- C = ( algSc ` W )
9:: |- E = ( .g ` W )
10:: |- P = ( chr ` K )
11:: |- ( ph -> ( Q C_ ZZ /\ Q e. Fin ) )
12:: |- F = { g | ( g : ZZ --> NN0 /\ ( g supp 0 ) = Q ) }
13:: |- ( ph -> P e. Prime )
14:: |- I = { x e. ( NN X. B ) | A. r e. S th }
15:: |- O = ( eval1 ` K )
16:: |- .- = ( -g ` R )
17:: |- T = ( f e. F |-> ( W gsum ( z e. ZZ |-> ( ( f ` z ) E ( X .- ( C ` ( ( ZRHom ` K ) ` z ) ) ) ) ) ) )
18:: |- ( th <-> ( ( 1st ` x ) D ( ( O ` ( 2nd ` x ) ) ` r ) )  = ( ( O ` ( 2nd ` x ) ) ` ( ( 1st ` x ) D r )  ) )

The explanation for the following lines.
1: K is a field, in our case it will be an algebraic closure of Fp, I think we'll need the Euclidean ring.
2: R=K[X], the polynomial ring in one variable
3: B are the elements of K[X]
4: The monomial X of K[X]
5: W is the multiplicative monoid of K[X] with the multiplication as operation (+g)
6: M, but with the Field K.
7: Group exponentiation of K. in CC ( 3 D 2 ) = ( 2 ^ 3 ) = 9
8: The scalars of K[X], which is "left scalar multiplication with K"
9: Same, but with the polynomial ring K[X], for example in Z[X] ( 2 E ( X + 1 ) ) = ( X^2+2X+1) (informally)
10,13: K with prime characteristic.
11: A finite subset of ZZ, in corresponds to  the following integers 0 ≤ ai ≤ ⌊pϕ(r) log n⌋ (11 INFO)
12: This is a bit more complicated, this is data necessary to define P. Here is an example: assume f that is in F with f(2)=3. Then the polynomial under T would be  ( x-2)^3, where the 2 is in K. This "transfers" information of the monic linear factors to the product of polynomials in K[X]
14: Definition of the introspective property. In the literature we have (e,f), we want to say that (e,f) is introspective when for all r-th primitive roots S, which by abuse of notation we also call r (in the literature this is \mu) the property 18 holds.
15: Polynomial evaluation of K[X]
16: Polynomial subtraction of K[X]
17: Define the elements of the literature script P as a product of finitely many linear factors, where the offsets are bounded by [11 INFO]
18:  (μ)e ≡ f (μe) in Fp in the literature.

Did I make any mistakes? Hint: I want to show that for every e \in Literature script E and every f \in Literature script P that e and f are introspective.
Claim 1(i) shows it for the monomials f=(x-a) and e=n/p, and e=p
Claim 1(ii) shows it for the product of f. In our case this corresponds to the pointwise sum of elements of F.
Claim 1(iii) shows it for the products of e. Here we need the properties of primitive roots and the fact that all elements of e are coprime to r. That's why \mu^e is also a primitive root, see the definition of  14 and recall that in this definition S stands for primitive roots.

If everything is fine I would like to formalise the statements and collect some more feedback before I start to formalising Claim 1. In our Case, transcribed it would be ( ph -> A. e e. ( (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) `` ( NN0 X. NN0 ))  A. f e. ( T `` F ) -> e I f )

Feedback would be immensely helpful, as I need to put several definitions in place, in particular I will need PerfectRings, PrimitiveRoots, maybe even roots of unity. I don't know yet what API I will need to formalise before I can tackle this statement.

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.

--
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+unsubscr...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/529b6b8d724cff6c3a66478989cc8f0a%40mail.eclipso.de.