OAI/NumberTheory/PrimePackets/ProjectivePeriods.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_projective_multiplier_zero line 122
  2. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_zero_multiplier_iff line 152
  3. theorem OAI.PrimeDegreePackets.root_invariant_of_nonzero_intrinsic_projective_period line 160
  4. theorem OAI.PrimeDegreePackets.intrinsicRootLeaf_projective_ergodic_alternative line 177
  5. def OAI.PrimeDegreePackets.rationalPointSpace line 203
  6. lemma OAI.PrimeDegreePackets.rationalPointSpace_mk line 206
  7. lemma OAI.PrimeDegreePackets.rationalPointSpace_clear_denominator line 211
  8. lemma OAI.PrimeDegreePackets.rationalPointSpace_no_coordinate_zero line 221
  9. instance OAI.PrimeDegreePackets.rationalPointSpace_finite line 229
  10. lemma OAI.PrimeDegreePackets.rationalPointSpace_finrank line 236
  11. lemma OAI.PrimeDegreePackets.rationalPointSpace_real_span line 245
  12. theorem OAI.PrimeDegreePackets.ae_rationalPointSpace_no_coordinate_zero line 258
  13. def OAI.PrimeDegreePackets.diagonalRationalAlgebra line 271
  14. instance OAI.PrimeDegreePackets.diagonalRationalAlgebra_module line 288
  15. instance OAI.PrimeDegreePackets.diagonalRationalAlgebra_tower line 298
  16. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_smul_val line 302
  17. def OAI.PrimeDegreePackets.diagonalRationalEval line 307
  18. lemma OAI.PrimeDegreePackets.diagonalRationalEval_injective line 313
  19. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_finite line 320
  20. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_coordinate_injective line 327
  21. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_isDomain line 342
  22. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_isField line 353
  23. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_finrank_dvd line 367
  24. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_prime_degree line 379
  25. lemma OAI.PrimeDegreePackets.rationalPointSpace_exists_nonzero_coordinates line 393
  26. theorem OAI.PrimeDegreePackets.ae_point_diagonalRationalAlgebra_isField line 405
  27. theorem OAI.PrimeDegreePackets.ae_point_diagonalRationalAlgebra_prime_degree line 416
  28. lemma OAI.PrimeDegreePackets.diagonalRationalEval_surjective line 431
  29. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_separates line 442
  30. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_eq_bot_of_repeated line 470
  31. theorem OAI.PrimeDegreePackets.ae_point_diagonalRationalAlgebra_repeated line 486
  32. def OAI.PrimeDegreePackets.diagonalCoordinateEmbedding line 504
  33. def OAI.PrimeDegreePackets.diagonalComplexEmbedding line 508
  34. lemma OAI.PrimeDegreePackets.diagonalComplexEmbedding_injective line 512
  35. theorem OAI.PrimeDegreePackets.diagonalComplexEmbedding_surjective line 525
  36. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_totallyReal line 549
  37. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_module_finrank_one line 569