OAI/NumberTheory/PrimePackets/AdelicCompactness.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PrimeDegreePackets.Adelic.primeFact line 11
2. def OAI.PrimeDegreePackets.Adelic.rationalLocalIntegers line 13
3. instance OAI.PrimeDegreePackets.Adelic.rationalIntegersOpen line 16
4. abbrev OAI.PrimeDegreePackets.Adelic.RationalFiniteAdeles line 21
5. lemma OAI.PrimeDegreePackets.Adelic.rational_eventually_integral line 24
6. def OAI.PrimeDegreePackets.Adelic.rationalFiniteEmbedding line 35
7. instance OAI.PrimeDegreePackets.Adelic.(instance at line 48) line 48
8. abbrev OAI.PrimeDegreePackets.Adelic.RationalAdeles line 50
9. abbrev OAI.PrimeDegreePackets.Adelic.TensorAdeles line 53
10. instance OAI.PrimeDegreePackets.Adelic.(instance at line 55) line 55
11. instance OAI.PrimeDegreePackets.Adelic.(instance at line 57) line 57
12. instance OAI.PrimeDegreePackets.Adelic.(instance at line 59) line 59
13. def OAI.PrimeDegreePackets.Adelic.torusPrincipalScalarSubgroup line 65
14. abbrev OAI.PrimeDegreePackets.Adelic.TorusQuotient line 70
15. instance OAI.PrimeDegreePackets.Adelic.tensorUnitsCommGroup line 73
16. abbrev OAI.PrimeDegreePackets.Adelic.LocalFiniteAdeles line 77
17. instance OAI.PrimeDegreePackets.Adelic.maximalOrdersOpen line 80
18. def OAI.PrimeDegreePackets.Adelic.integerRatBasis line 86
19. lemma OAI.PrimeDegreePackets.Adelic.localIntegralSpan_integerRatBasis line 90
20. lemma OAI.PrimeDegreePackets.Adelic.field_eventually_integral line 97
21. def OAI.PrimeDegreePackets.Adelic.localFiniteEmbedding line 115
22. instance OAI.PrimeDegreePackets.Adelic.(instance at line 123) line 123
23. instance OAI.PrimeDegreePackets.Adelic.(instance at line 125) line 125
24. instance OAI.PrimeDegreePackets.Adelic.(instance at line 127) line 127
25. lemma OAI.PrimeDegreePackets.Adelic.localFiniteEmbedding_apply line 130
26. lemma OAI.PrimeDegreePackets.Adelic.integerRatBasis_coordinate_mem line 134
27. def OAI.PrimeDegreePackets.Adelic.finiteCoordinates line 143
28. lemma OAI.PrimeDegreePackets.Adelic.finiteCoordinates_apply line 148
29. lemma OAI.PrimeDegreePackets.Adelic.continuous_finiteCoordinates line 152
30. def OAI.PrimeDegreePackets.Adelic.fromFiniteCoordinates line 160
31. lemma OAI.PrimeDegreePackets.Adelic.finiteCoordinates_fromFiniteCoordinates line 175
32. lemma OAI.PrimeDegreePackets.Adelic.fromFiniteCoordinates_finiteCoordinates line 182
33. def OAI.PrimeDegreePackets.Adelic.finiteScalarEmbedding line 188
34. lemma OAI.PrimeDegreePackets.Adelic.finiteScalarEmbedding_apply line 199
35. def OAI.PrimeDegreePackets.Adelic.finiteScalarAlgHom line 203
36. instance OAI.PrimeDegreePackets.Adelic.(instance at line 213) line 213
37. instance OAI.PrimeDegreePackets.Adelic.(instance at line 217) line 217
38. lemma OAI.PrimeDegreePackets.Adelic.finite_smul_apply line 224
39. def OAI.PrimeDegreePackets.Adelic.finiteCoordinatesLinear line 230
40. def OAI.PrimeDegreePackets.Adelic.finiteCoordinatesEquiv line 247
41. abbrev OAI.PrimeDegreePackets.Adelic.FiniteTensorAdeles line 259
42. def OAI.PrimeDegreePackets.Adelic.finiteTensorMap line 262
43. lemma OAI.PrimeDegreePackets.Adelic.finiteTensorMap_tmul_apply line 267
44. lemma OAI.PrimeDegreePackets.Adelic.finiteCoordinates_finiteTensorMap line 274
45. def OAI.PrimeDegreePackets.Adelic.finiteTensorEquiv line 298
46. abbrev OAI.PrimeDegreePackets.Adelic.RealAlgebra line 314
47. instance OAI.PrimeDegreePackets.Adelic.(instance at line 315) line 315
48. instance OAI.PrimeDegreePackets.Adelic.(instance at line 317) line 317
49. instance OAI.PrimeDegreePackets.Adelic.(instance at line 318) line 318
50. instance OAI.PrimeDegreePackets.Adelic.(instance at line 320) line 320
51. instance OAI.PrimeDegreePackets.Adelic.(instance at line 322) line 322
52. abbrev OAI.PrimeDegreePackets.Adelic.ModelAdeles line 326
53. def OAI.PrimeDegreePackets.Adelic.tensorProdEquiv line 329
54. def OAI.PrimeDegreePackets.Adelic.tensorModelEquiv line 336
55. lemma OAI.PrimeDegreePackets.Adelic.tensorModelEquiv_tmul line 342
56. def OAI.PrimeDegreePackets.Adelic.modelCoordinates line 347
57. lemma OAI.PrimeDegreePackets.Adelic.modelCoordinates_tensorModelEquiv line 352
58. lemma OAI.PrimeDegreePackets.Adelic.continuous_modelCoordinates line 382
59. lemma OAI.PrimeDegreePackets.Adelic.tensorModelEquiv_symm_eq_coordinates line 390
60. lemma OAI.PrimeDegreePackets.Adelic.continuous_tensorModelEquiv_symm line 398
61. lemma OAI.PrimeDegreePackets.Adelic.local_vector_denominator line 409
62. lemma OAI.PrimeDegreePackets.Adelic.local_principal_clear_denominators line 417
63. def OAI.PrimeDegreePackets.Adelic.localUnit line 455
64. lemma OAI.PrimeDegreePackets.Adelic.localUnit_val line 459
65. lemma OAI.PrimeDegreePackets.Adelic.localUnit_eventually_integral line 463
66. lemma OAI.PrimeDegreePackets.Adelic.local_unit_smul_order line 470
67. theorem OAI.PrimeDegreePackets.Adelic.finite_idele_ideal_patch line 485
68. abbrev OAI.PrimeDegreePackets.Adelic.IntegralFiniteUnits line 543
69. def OAI.PrimeDegreePackets.Adelic.integralFiniteUnit line 546
70. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteUnit_apply line 553
71. lemma OAI.PrimeDegreePackets.Adelic.continuous_integralFiniteUnit line 557
72. abbrev OAI.PrimeDegreePackets.Adelic.finitePrincipal line 566
73. abbrev OAI.PrimeDegreePackets.Adelic.finiteScalar line 568
74. theorem OAI.PrimeDegreePackets.Adelic.finite_idele_finite_representatives line 573
75. def OAI.PrimeDegreePackets.Adelic.realTensorMap line 619
76. lemma OAI.PrimeDegreePackets.Adelic.realTensorMap_tmul line 624
77. lemma OAI.PrimeDegreePackets.Adelic.realTensorMap_bijective line 628
78. def OAI.PrimeDegreePackets.Adelic.realTensorEquiv line 656
79. lemma OAI.PrimeDegreePackets.Adelic.continuous_realTensorEquiv_symm line 661
80. def OAI.PrimeDegreePackets.Adelic.chooseOrderedEmbeddings line 667
81. def OAI.PrimeDegreePackets.Adelic.fullLog line 677
82. lemma OAI.PrimeDegreePackets.Adelic.continuous_fullLog line 680
83. def OAI.PrimeDegreePackets.Adelic.signedExpUnit line 688
84. lemma OAI.PrimeDegreePackets.Adelic.continuous_signedExpUnit line 703
85. abbrev OAI.PrimeDegreePackets.Adelic.splitScalar line 712
86. abbrev OAI.PrimeDegreePackets.Adelic.splitPrincipal line 714
87. lemma OAI.PrimeDegreePackets.Adelic.splitUnit_nonzero line 717
88. lemma OAI.PrimeDegreePackets.Adelic.exists_compact_log_representatives line 725
89. theorem OAI.PrimeDegreePackets.Adelic.real_split_compact_representatives line 746
90. def OAI.PrimeDegreePackets.Adelic.integralUnitFinite line 808
91. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteUnit_integralUnitFinite line 816
92. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteUnit_mul line 823
93. def OAI.PrimeDegreePackets.Adelic.splitTensorEquiv line 831
94. lemma OAI.PrimeDegreePackets.Adelic.continuous_splitTensorEquiv_symm line 837
95. def OAI.PrimeDegreePackets.Adelic.ideleEquiv line 845
96. lemma OAI.PrimeDegreePackets.Adelic.continuous_ideleEquiv_symm line 850
97. abbrev OAI.PrimeDegreePackets.Adelic.tensorPrincipal line 860
98. abbrev OAI.PrimeDegreePackets.Adelic.tensorScalar line 862
99. lemma OAI.PrimeDegreePackets.Adelic.ideleEquiv_tensorPrincipal line 865
100. lemma OAI.PrimeDegreePackets.Adelic.ideleEquiv_tensorScalar line 878
101. def OAI.PrimeDegreePackets.Adelic.localQuotientMap line 893
102. lemma OAI.PrimeDegreePackets.Adelic.continuous_localQuotientMap line 898
103. lemma OAI.PrimeDegreePackets.Adelic.localQuotientMap_principal line 903
104. lemma OAI.PrimeDegreePackets.Adelic.localQuotientMap_scalar line 912
105. theorem OAI.PrimeDegreePackets.Adelic.adelic_torus_quotient_compact line 925