Implementation of Tate's algorithm for elliptic curves in mathlib4:
- Some personal ports of Group/Int/Nat/Ring lemmas
- A definition of extended natural numbers 'ENat.lean'
- An environment for the models and quantities associated to elliptic curves 'Model.lean'
- An extension of commutative rings with a normalized valuation 'ValuedRing.lean'
- An implementation of Tate's algorithm over the integers 'TateInt.lean'
- An implementation of Tate's algorithm over the rings 'TateRing.lean'
- Tests to compare our output with LMFDB's data 'test/Test.lean'
- An implementation of the Kronecker symbol for integers 'Kronecker.lean'