OAI/NumberTheory/SiegelZeros/Differentials/RectangleCotangentBasis.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SiegelZeros.WeightedTorusJets.W25.Active line 17
  2. def OAI.SiegelZeros.WeightedTorusJets.W25.activeBoxIndex line 19
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W25.boxExponent_activeBoxIndex line 27
  4. def OAI.SiegelZeros.WeightedTorusJets.W25.quotientFirstCoefficient line 32
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientFirstCoefficient_mk line 37
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientFirstCoefficient_eq_zero_of_mem_square line 44
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W25.mem_augmentationSquare_of_coefficients_zero line 55
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W25.mem_augmentationSquare_iff line 98
  9. def OAI.SiegelZeros.WeightedTorusJets.W25.augmentationFirstCoordinates line 110
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentationFirstCoordinates_product_zero line 115
  11. def OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentCoordinates line 123
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentCoordinates_toCotangent line 128
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentCoordinates_injective line 133
  14. def OAI.SiegelZeros.WeightedTorusJets.W25.coordinateCotangentClass line 144
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentCoordinates_coordinate line 152
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentCoordinates_surjective line 166
  17. def OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentEquiv line 175
  18. def OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentBasis line 181
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W25.rectangleCotangentBasis_eq_coordinate line 185
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W25.coordinateCotangentClass_span line 197
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W25.finrank_rectangleCotangent line 207