Tate's algorithm

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'