OAI/NumberTheory/PrimePackets/AdelicContinuity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.absoluteNormalizedMatrix line 11
2. lemma OAI.PrimeDegreePackets.Adelic.absoluteNormalizedMatrix_det line 14
3. lemma OAI.PrimeDegreePackets.Adelic.absoluteNormalizedMatrix_det_pos_iff line 18
4. def OAI.PrimeDegreePackets.Adelic.realSLNormalize line 26
5. lemma OAI.PrimeDegreePackets.Adelic.realSLNormalize_projective line 38
6. lemma OAI.PrimeDegreePackets.Adelic.continuous_absoluteNormalizedMatrix line 63
7. lemma OAI.PrimeDegreePackets.Adelic.continuous_realSLNormalize line 68
8. lemma OAI.PrimeDegreePackets.Adelic.ambientEquiv_realSLNormalize line 82
9. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGroup_isOpen line 89
10. lemma OAI.PrimeDegreePackets.Adelic.continuous_rowRegular line 102
11. lemma OAI.PrimeDegreePackets.Adelic.continuous_rowRegularUnits line 112
12. lemma OAI.PrimeDegreePackets.Adelic.continuous_adelicIdelePoint line 117
13. lemma OAI.PrimeDegreePackets.Adelic.continuous_adelicTorusPoint line 150