OAI/NumberTheory/PrimePackets/AdelicPacketPoints.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.diagonalUnits line 11
2. def OAI.PrimeDegreePackets.Adelic.adelicMatrixPoint line 14
3. def OAI.PrimeDegreePackets.Adelic.realMatrixPoint line 18
4. lemma OAI.PrimeDegreePackets.Adelic.realMatrixPoint_eq_of_projective_eq line 20
5. lemma OAI.PrimeDegreePackets.Adelic.realBasisGL_basisChange line 24
6. lemma OAI.PrimeDegreePackets.Adelic.realBasisGL_latticeBasis line 38
7. lemma OAI.PrimeDegreePackets.Adelic.exists_SL_normalizedLattice_projective line 44
8. lemma OAI.PrimeDegreePackets.Adelic.ambientEquiv_latticePoint_rightAction line 71
9. lemma OAI.PrimeDegreePackets.Adelic.matrixFullLattice_basis_reduction line 84
10. lemma OAI.PrimeDegreePackets.Adelic.adelicMatrixPoint_reduction line 103
11. lemma OAI.PrimeDegreePackets.Adelic.adelicMatrixPoint_basis_reduction line 117
12. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_real_matrix line 125
13. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_finite_matrix line 137
14. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_translate line 149
15. lemma OAI.PrimeDegreePackets.Adelic.specialLinear_diagonal_preimage line 166
16. lemma OAI.PrimeDegreePackets.Adelic.diagonalUnits_of_SL line 178