OAI/NumberTheory/PrimePackets/RationalLattices.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.pointLattice_basis_nonempty line 121
  2. def OAI.PrimeDegreePackets.pointLatticeBasis line 127
  3. def OAI.PrimeDegreePackets.rationalPointRealization line 130
  4. def OAI.PrimeDegreePackets.rationalPointPullback line 134
  5. def OAI.PrimeDegreePackets.rationalPointPullbackMap line 138
  6. lemma OAI.PrimeDegreePackets.rationalPointPullbackMap_bijective line 145
  7. def OAI.PrimeDegreePackets.rationalPointPullbackEquiv line 163
  8. lemma OAI.PrimeDegreePackets.rationalPointPullback_spans line 168
  9. def OAI.PrimeDegreePackets.rationalPointFullLattice line 182
  10. lemma OAI.PrimeDegreePackets.rationalPointFullLattice_image line 188
  11. lemma OAI.PrimeDegreePackets.pointLattice_injective line 207
  12. lemma OAI.PrimeDegreePackets.rationalPoint_units_invariant line 214
  13. theorem OAI.PrimeDegreePackets.rationalPoint_orderedLog_le_period line 239
  14. theorem OAI.PrimeDegreePackets.rationalPoint_period_isZLattice line 256
  15. theorem OAI.PrimeDegreePackets.rationalPoint_diagonalOrbit_isCompact line 271
  16. def OAI.PrimeDegreePackets.fieldRatLinearEquiv line 291
  17. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_fullDegree_period line 295
  18. theorem OAI.PrimeDegreePackets.diagonalRationalAlgebra_fullDegree_compact line 333
  19. theorem OAI.PrimeDegreePackets.ae_scalar_commutant_or_compact line 346
  20. def OAI.PrimeDegreePackets.AlgebraicReal line 363
  21. instance OAI.PrimeDegreePackets.algebraicReal_countable line 365
  22. abbrev OAI.PrimeDegreePackets.AlgebraicFrame line 368
  23. lemma OAI.PrimeDegreePackets.diagonalRationalAlgebra_coordinate_algebraic line 370
  24. theorem OAI.PrimeDegreePackets.exists_algebraicFrame_of_fullDegree line 381
  25. def OAI.PrimeDegreePackets.algebraicFrameClass line 413
  26. lemma OAI.PrimeDegreePackets.algebraicFrameClass_sameOrbit line 417
  27. lemma OAI.PrimeDegreePackets.fullDegree_mem_algebraicFrameClass line 440
  28. lemma OAI.PrimeDegreePackets.orbitQuotientMap_injective line 453
  29. lemma OAI.PrimeDegreePackets.range_orbitQuotientMap line 464
  30. lemma OAI.PrimeDegreePackets.orbitQuotientMap_measurableEmbedding line 475
  31. theorem OAI.PrimeDegreePackets.measureEntropy_eq_zero_of_ae_mem_fullPeriodOrbit line 484
  32. def OAI.PrimeDegreePackets.FullDegreeFrame line 521
  33. instance OAI.PrimeDegreePackets.fullDegreeFrame_countable line 526
  34. def OAI.PrimeDegreePackets.fullDegreeFramePoint line 533
  35. lemma OAI.PrimeDegreePackets.fullDegreeFramePoint_spec line 536
  36. lemma OAI.PrimeDegreePackets.fullDegreeFramePoint_period line 541
  37. theorem OAI.PrimeDegreePackets.fullDegree_mem_range_compact_orbits line 548
  38. lemma OAI.PrimeDegreePackets.diagonalOrbit_rightAction_mem_iff line 556
  39. lemma OAI.PrimeDegreePackets.measurableSet_diagonalOrbit_fullPeriod line 567
  40. theorem OAI.PrimeDegreePackets.ae_not_mem_fullPeriodOrbit_of_positive_entropy line 574
  41. theorem OAI.PrimeDegreePackets.ae_scalar_diagonalRationalAlgebra_of_positive_entropy line 598