search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

Theorem 6.6 Aks Inequality #4038

Closed metakunt closed 1 month ago

metakunt commented 1 month ago

@tirix sorry, I have lately been very busy so I couldn't really contribute much to the blueprint. I have formalized an inequality for Theorem 6.6 Claim 7 as discussed in https://github.com/tirix/metamath-blueprints/pull/7

metakunt commented 1 month ago

Also we need to make inequality right after (6.6)

\lfloor \sqrt{\vert\bar{\mathcal{E }}\vert \log n} \rfloor \geq 1

strict to apply 2ap1caineq since the author is obviously a moronic moron.

tirix commented 1 month ago

No problem! Nice proof.

I'll see if I can formalize some theorems towards Galois Theory. On the way, one step will also be finite fields.