OAI/Combinatorics/Progressions/Lattices/NativeIntegerHalving.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeIntegerExpansion.ofProduct line 16
  2. def OAI.Erdos3.NativeIntegerExpansion.mul line 63
  3. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.trans line 106
  4. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_trans_budget line 144
  5. def OAI.Erdos3.NativeIntegerExpansion.constOne line 169
  6. theorem OAI.Erdos3.NativeIntegerExpansion.exists_mul_budget line 174
  7. theorem OAI.Erdos3.card_product_le_exp_two line 200
  8. theorem OAI.Erdos3.complex_tensor_cross_product line 207
  9. def OAI.Erdos3.NativeIntegerExpansion.tensorCrossProduct line 212
  10. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.tensor line 226
  11. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_tensor_budget line 246
  12. theorem OAI.Erdos3.NativeIntegerExpansion.exists_fin_prod_budget line 281
  13. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_cancel_left_tensor_budget line 321
  14. theorem OAI.Erdos3.RationalTorus.residueNiltest_eval line 378
  15. theorem OAI.Erdos3.exists_coordinate_residue_expansion line 389
  16. def OAI.Erdos3.pairParityIndicator line 402
  17. theorem OAI.Erdos3.pairParityIndicator_product line 405
  18. theorem OAI.Erdos3.exists_pairParityIndicator_expansion line 421
  19. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_tensor_power_budget line 451
  20. theorem OAI.Erdos3.NativeIntegerExpansion.exists_halving_expansion line 502