OAI/AlgebraicGeometry/Seshadri/Interpolation/CyclicLattices.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Interpolation.latticeHeight line 10
2. def OAI.MaximalSeshadri.Interpolation.latticeCoord line 12
3. theorem OAI.MaximalSeshadri.Interpolation.latticeCoord_reconstruct line 16
4. theorem OAI.MaximalSeshadri.Interpolation.latticeCoord_injOn line 30
5. def OAI.MaximalSeshadri.Interpolation.cyclicTorusPoint line 42
6. theorem OAI.MaximalSeshadri.Interpolation.cyclicTorusPoint_character line 45
7. theorem OAI.MaximalSeshadri.Interpolation.cyclicTorusPoint_injective line 54
8. def OAI.MaximalSeshadri.Interpolation.latticeAffine line 67
9. theorem OAI.MaximalSeshadri.Interpolation.latticeCoord_cast line 78
10. theorem OAI.MaximalSeshadri.Interpolation.latticeAffine_det line 92
11. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.congr line 104
12. theorem OAI.MaximalSeshadri.Interpolation.MomentJetZero.nonzeroSupport line 114
13. theorem OAI.MaximalSeshadri.Interpolation.latticeCoord_cast_complex line 125
14. theorem OAI.MaximalSeshadri.Interpolation.lattice_coordinate_moments line 141
15. theorem OAI.MaximalSeshadri.Interpolation.lattice_moments line 163
16. theorem OAI.MaximalSeshadri.Interpolation.latticeAffine_snd_sub line 176
17. theorem OAI.MaximalSeshadri.Interpolation.sqrt_mul_div line 183