OAI/NumberTheory/SingleFold/FiniteGeneration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SingleFold.HeightDescent.finitely_generated line 11
2. instance OAI.SingleFold.CurveRank.(instance at line 55) line 55
3. lemma OAI.SingleFold.CurveRank.canonical_parallelogram line 65
4. def OAI.SingleFold.CurveRank.representatives line 74
5. lemma OAI.SingleFold.CurveRank.representatives_card line 78
6. lemma OAI.SingleFold.CurveRank.representatives_cover line 92
7. instance OAI.SingleFold.CurveRank.(instance at line 102) line 102