search

mortarsanjaya / imo-A-and-N

IMO SL Formalization
Apache License 2.0
3 stars 0 forks source link

2020 N5 extra: Add distinction results and construction of a wide non-zero map. #11

Closed mortarsanjaya closed 2 years ago

mortarsanjaya commented 2 years ago

The distinction result is on WIP. The wide non-zero map construction requires Dirichlet's theorem on arithmetic progression, so either make that an axiom for a moment, or just wait.

mortarsanjaya commented 2 years ago

Distinction result is complete. We wait for Dirichlet's theorem. We also need the periodicity of Legendre symbol (w.r.t the second argument) to be implemented to start the construction.

mortarsanjaya commented 2 years ago

As the API for the Jacobi symbol now exists, the wide non-zero map construction can be done. It is now complete.