OAI/NumberTheory/SiegelZeros/LocalAlgebra/HeightFourLength.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W24.augmentation_surjective line 23
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W24.simple_annihilator_eq_augmentation_kernel line 27
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W24.simple_smul_eq_augmentation_smul line 36
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W24.simple_over_coefficient_field line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W24.length_eq_coefficient_length line 60
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W24.module_length_eq_finrank_of_augmentation line 84
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ring_length_eq_finrank_of_augmentation line 95
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentation_algebraMap line 107
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W25.intrinsic_length_truncatedQuotient line 112
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W24.intrinsic_length_ringEquiv line 135
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W24.length_le_quotient_of_surjective line 143
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W24.intrinsic_length_rectangleJet line 162
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W24.rectangleResidue_polynomialRectangleEquiv line 169
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W24.rectangleAugmentation_eq_map line 183
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W24.rectangleAugmentation_pow_eq_bot line 197
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W24.selectedFirst_polynomialRectangleEquiv line 204
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W24.rectangle_mem_square_of_coefficients_zero line 220
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W24.selectedCotangent_coordinates_injective line 240
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W24.selectedTaylorCotangent_surjective_of_coordinate_injective line 272
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W24.local_rectangularJet_surjective line 308
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W24.component_length_lower_of_derivative_evaluation line 368
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W24.selected_component_length_lower line 398
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W24.generic_component_length_lower line 438
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W24.identity_component_length_lower line 460
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W21.height_four_component_length_lower line 492