OAI/NumberTheory/PrimePackets/AdelicPacket.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_tmul line 11
2. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_tensor_map line 19
3. lemma OAI.PrimeDegreePackets.Adelic.realTensorMap_coordinates line 36
4. lemma OAI.PrimeDegreePackets.Adelic.real_regular_diagonalization line 53
5. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_finite_at line 68
6. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_real_component line 89
7. lemma OAI.PrimeDegreePackets.Adelic.rowRegular_finite_component line 104
8. def OAI.PrimeDegreePackets.Adelic.finiteRegular line 120
9. lemma OAI.PrimeDegreePackets.Adelic.finiteRegular_at line 125
10. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_finiteRegular line 136
11. lemma OAI.PrimeDegreePackets.Adelic.matrixFullLattice_finiteRegular_locallyHomothetic line 165
12. def OAI.PrimeDegreePackets.Adelic.assembleFiniteIdele line 178
13. lemma OAI.PrimeDegreePackets.Adelic.localUnit_assembleFiniteIdele line 192
14. lemma OAI.PrimeDegreePackets.Adelic.completedLattice_eq_of_carrier_eq line 197
15. lemma OAI.PrimeDegreePackets.Adelic.finiteIdele_realizes_local_homothety line 202