OAI/NumberTheory/SiegelZeros/LocalAlgebra/SelectedLengthContradiction.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W25.truncationIdeal line 22
  2. abbrev OAI.SiegelZeros.WeightedTorusJets.W25.Box line 25
  3. def OAI.SiegelZeros.WeightedTorusJets.W25.boxExponent line 27
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W25.boxExponent_apply line 30
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W25.boxExponent_injective line 33
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W25.mem_truncationIdeal_iff line 40
  7. def OAI.SiegelZeros.WeightedTorusJets.W25.boxCoefficients line 56
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W25.boxCoefficients_apply line 61
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W25.ker_boxCoefficients line 64
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W25.boxCoefficients_surjective line 87
  11. def OAI.SiegelZeros.WeightedTorusJets.W25.truncatedQuotientEquiv line 96
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W25.finrank_truncatedQuotient line 101
  13. instance OAI.SiegelZeros.WeightedTorusJets.W25.truncatedQuotient_finite line 108
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W25.coefficientField_length_truncatedQuotient line 113
  15. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.finite_value_of_bound line 126
  16. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.finite_length_of_bound line 135
  17. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.enat_length_bounds_incompatible line 139
  18. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.module_length_bounds_incompatible line 151
  19. abbrev OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedQuotient line 164
  20. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedQuotient_coefficient_length line 167
  21. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.coefficient_length_bounds_incompatible line 177
  22. def OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedFinset line 199
  23. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.mem_selectedFinset line 203
  24. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedFinset_card line 208
  25. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedSet_card_le_three line 213
  26. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedCutoffs_product line 217
  27. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.selectedCutoffs_length_bounds_incompatible line 234
  28. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.generic_selectedCutoffs_length_bounds_incompatible line 245
  29. theorem OAI.SiegelZeros.WeightedTorusJets.RectangleNumerics.full_length_bounds_incompatible line 256