OAI/NumberTheory/PrimePackets/AdelicRepresentation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.rowRegular line 12
2. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_apply line 24
3. lemma OAI.PrimeDegreePackets.Adelic.vecMul_rowRegular line 29
4. def OAI.PrimeDegreePackets.Adelic.rowRegularUnits line 36
5. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_baseChange line 40
6. def OAI.PrimeDegreePackets.Adelic.adelicRegular line 51
7. def OAI.PrimeDegreePackets.Adelic.realBasisGL line 57
8. lemma OAI.PrimeDegreePackets.Adelic.realBasisGL_apply line 62
9. def OAI.PrimeDegreePackets.Adelic.adelicPacketSupport line 69
10. def OAI.PrimeDegreePackets.Adelic.matrixFullLattice line 77
11. lemma OAI.PrimeDegreePackets.Adelic.matrixFullLattice_carrier line 81
12. lemma OAI.PrimeDegreePackets.Adelic.matrixFullLattice_completed line 86
13. def OAI.PrimeDegreePackets.Adelic.ambientEquiv line 92
14. lemma OAI.PrimeDegreePackets.Adelic.ambientEquiv_mk line 96