OAI/NumberTheory/PowerFree/PairProjections.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.positiveToPairHom line 12
  2. theorem OAI.QuarticPowerFree.positiveToPairHom_apply line 16
  3. theorem OAI.QuarticPowerFree.positiveToPair_option line 20
  4. theorem OAI.QuarticPowerFree.pairConeA_homogeneous line 36
  5. theorem OAI.QuarticPowerFree.pairConeB_homogeneous line 46
  6. def OAI.QuarticPowerFree.pairConeN line 56
  7. theorem OAI.QuarticPowerFree.pairConeN_homogeneous line 61
  8. theorem OAI.QuarticPowerFree.pairConeToRoot_N line 72
  9. theorem OAI.QuarticPowerFree.rootPair_projection_homogeneous_lift line 78
  10. theorem OAI.QuarticPowerFree.pairConeToRoot_surjective line 108
  11. theorem OAI.QuarticPowerFree.pairConeToRoot_kernel line 117
  12. theorem OAI.QuarticPowerFree.rootPair_bounded_cone_kernel line 129
  13. theorem OAI.QuarticPowerFree.finrank_map_eq_of_kernel_eq line 191
  14. theorem OAI.QuarticPowerFree.finrank_map_quotient_kernel line 204
  15. theorem OAI.QuarticPowerFree.rootPair_actual_hilbert_uniform line 216
  16. theorem OAI.QuarticPowerFree.weightedSpace_mul_mem line 276
  17. theorem OAI.QuarticPowerFree.weightedSpace_one line 288
  18. theorem OAI.QuarticPowerFree.weightedSpace_pow_mem line 294
  19. theorem OAI.QuarticPowerFree.weightedSpace_prod_mem line 301
  20. theorem OAI.QuarticPowerFree.weightedSpace_mono line 313
  21. theorem OAI.QuarticPowerFree.weightedSpace_aeval line 319
  22. theorem OAI.QuarticPowerFree.totalSpace_aeval line 339