OAI/NumberTheory/SiegelZeros/Selection/RestrictWeightSortedEquiv.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.exists_first_greedy_jet_rows line 22
  2. theorem OAI.SiegelZeros.WeightedTorusJets.basis_nat_sum_injective line 75
  3. theorem OAI.SiegelZeros.WeightedTorusJets.basis_nat_sum_mul_injective line 84
  4. theorem OAI.SiegelZeros.WeightedTorusJets.basis_fin_sum_mul_injective line 94
  5. theorem OAI.SiegelZeros.WeightedTorusJets.exists_first_greedy_jet_rows_of_sorted_enumeration line 104
  6. theorem OAI.SiegelZeros.WeightedTorusJets.source_character_fixed_greedy_determinant_divisibility_of_field_ne line 157
  7. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_congr_prefix line 238
  8. theorem OAI.SiegelZeros.WeightedTorusJets.weight_sorted_equiv_mem_iff_lt_card line 257
  9. def OAI.SiegelZeros.WeightedTorusJets.restrictWeightSortedEquiv line 280
  10. theorem OAI.SiegelZeros.WeightedTorusJets.restrictWeightSortedEquiv_apply line 289
  11. theorem OAI.SiegelZeros.WeightedTorusJets.restrictWeightSortedEquiv_monotone line 294
  12. theorem OAI.SiegelZeros.WeightedTorusJets.extend_restrictWeightSortedEquiv_eq line 301
  13. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_restrictWeightSortedEquiv line 309
  14. theorem OAI.SiegelZeros.WeightedTorusJets.weight_sorted_equiv_image_range line 324
  15. theorem OAI.SiegelZeros.WeightedTorusJets.span_global_weight_cutoff_eq_top line 339
  16. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_global_weight_cutoff line 349
  17. theorem OAI.SiegelZeros.WeightedTorusJets.source_character_global_greedy_determinant_divisibility line 367
  18. theorem OAI.SiegelZeros.SiegelJets.norm_det_le_prod_norm line 470
  19. theorem OAI.SiegelZeros.SiegelJets.norm_det_le_of_entry_bound line 493
  20. theorem OAI.SiegelZeros.SiegelJets.log_norm_det_le_of_entry_bound line 517
  21. theorem OAI.SiegelZeros.SiegelJets.log_norm_det_archimedean line 532
  22. theorem OAI.SiegelZeros.SiegelJets.log_norm_map_det_archimedean line 548