OAI/Algebra/FormalGroup/Honda/Canonical.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HeightThree.CanonicalUniversality.honda_frobenius line 10
2. def OAI.HeightThree.CanonicalUniversality.data line 23
3. theorem OAI.HeightThree.CanonicalUniversality.reducedHonda_isUniversal line 43
4. theorem OAI.HeightThree.CanonicalUniversality.canonical_hasUniversalHeightCoordinates line 48