OAI/NumberTheory/PrimePackets/AdelicReduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.IntegralFiniteGL line 13
2. lemma OAI.PrimeDegreePackets.Adelic.localCoordinates_basisChange line 17
3. lemma OAI.PrimeDegreePackets.Adelic.localMatrixLattice_basisChange line 31
4. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteAt_of_lattice_eq line 43
5. lemma OAI.PrimeDegreePackets.Adelic.completedLattice_integralSpan_basis line 82
6. theorem OAI.PrimeDegreePackets.Adelic.finite_matrix_rational_reduction line 88