OAI/NumberTheory/Jacobsthal/Siegel/RestrictWeightSortedEquiv.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.exists_first_greedy_jet_rows line 24
  2. theorem OAI.Erdos970.WeightedTorusJets.basis_nat_sum_injective line 77
  3. theorem OAI.Erdos970.WeightedTorusJets.basis_nat_sum_mul_injective line 86
  4. theorem OAI.Erdos970.WeightedTorusJets.basis_fin_sum_mul_injective line 96
  5. theorem OAI.Erdos970.WeightedTorusJets.exists_first_greedy_jet_rows_of_sorted_enumeration line 106
  6. theorem OAI.Erdos970.WeightedTorusJets.source_character_fixed_greedy_determinant_divisibility_of_field_ne line 159
  7. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_congr_prefix line 240
  8. theorem OAI.Erdos970.WeightedTorusJets.weight_sorted_equiv_mem_iff_lt_card line 259
  9. def OAI.Erdos970.WeightedTorusJets.restrictWeightSortedEquiv line 282
  10. theorem OAI.Erdos970.WeightedTorusJets.restrictWeightSortedEquiv_apply line 291
  11. theorem OAI.Erdos970.WeightedTorusJets.restrictWeightSortedEquiv_monotone line 296
  12. theorem OAI.Erdos970.WeightedTorusJets.extend_restrictWeightSortedEquiv_eq line 303
  13. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_restrictWeightSortedEquiv line 311
  14. theorem OAI.Erdos970.WeightedTorusJets.weight_sorted_equiv_image_range line 326
  15. theorem OAI.Erdos970.WeightedTorusJets.span_global_weight_cutoff_eq_top line 341
  16. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_global_weight_cutoff line 351
  17. theorem OAI.Erdos970.WeightedTorusJets.source_character_global_greedy_determinant_divisibility line 369
  18. theorem OAI.Erdos970.SiegelJets.norm_det_le_prod_norm line 472
  19. theorem OAI.Erdos970.SiegelJets.norm_det_le_of_entry_bound line 495
  20. theorem OAI.Erdos970.SiegelJets.log_norm_det_le_of_entry_bound line 519
  21. theorem OAI.Erdos970.SiegelJets.log_norm_det_archimedean line 534
  22. theorem OAI.Erdos970.SiegelJets.log_norm_map_det_archimedean line 550