OAI/NumberTheory/PrimePackets/AdelicLattices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.finiteCoefficientRow line 12
2. def OAI.PrimeDegreePackets.Adelic.FiniteIntegralRow line 17
3. def OAI.PrimeDegreePackets.Adelic.finiteCompletedMatrixLattice line 21
4. def OAI.PrimeDegreePackets.Adelic.finiteGlobalMatrixLattice line 26
5. lemma OAI.PrimeDegreePackets.Adelic.mem_finiteCompletedMatrixLattice_iff line 30
6. def OAI.PrimeDegreePackets.Adelic.rowBasisChange line 42
7. lemma OAI.PrimeDegreePackets.Adelic.vecMul_rowBasisChange line 49
8. lemma OAI.PrimeDegreePackets.Adelic.finiteCoefficientRow_basisChange line 55
9. lemma OAI.PrimeDegreePackets.Adelic.finiteIntegralRow_latticeBasis_iff line 65
10. theorem OAI.PrimeDegreePackets.Adelic.every_full_lattice_occurs line 91