OAI/NumberTheory/PowerFree/StoppingTrees.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.treeLevel line 14
  2. theorem OAI.QuarticPowerFree.treeLevel_card_le line 19
  3. theorem OAI.QuarticPowerFree.cardinal_tree_stopping line 33
  4. theorem OAI.QuarticPowerFree.physical_initial_states line 79
  5. theorem OAI.QuarticPowerFree.card_nonsingular_roots_indexed line 95
  6. theorem OAI.QuarticPowerFree.card_smooth_patch_indexed line 127
  7. def OAI.QuarticPowerFree.IntegerPatch.goodResidues line 161
  8. theorem OAI.QuarticPowerFree.IntegerPatch.card_goodResidues line 168
  9. def OAI.QuarticPowerFree.residueTuple line 215
  10. theorem OAI.QuarticPowerFree.residueTuple_eq_iff line 218
  11. theorem OAI.QuarticPowerFree.IntegerPatch.eval_equation_zero line 231
  12. theorem OAI.QuarticPowerFree.IntegerPatch.residue_mem_iff line 238
  13. theorem OAI.QuarticPowerFree.card_filter_coe_finset line 245
  14. theorem OAI.QuarticPowerFree.IntegerPatch.card_bad_residue_tuple line 251
  15. theorem OAI.QuarticPowerFree.IntegerPatch.card_goodResidues_zmod_le line 266
  16. theorem OAI.QuarticPowerFree.IntegerPatch.card_residue_image line 283