OAI/NumberTheory/PrimePackets/AdelicCanonicalAllowed.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Adelic.realPGLToSL line 11
2. lemma OAI.PrimeDegreePackets.Adelic.realPGLToSL_projective line 18
3. lemma OAI.PrimeDegreePackets.Adelic.realPGLToSL_toPGL line 23
4. lemma OAI.PrimeDegreePackets.Adelic.continuous_realPGLToSL line 28
5. lemma OAI.PrimeDegreePackets.Adelic.real_torus_diagonal line 31
6. lemma OAI.PrimeDegreePackets.Adelic.real_torus_identity_positive line 56
7. theorem OAI.PrimeDegreePackets.Adelic.canonical_real_diagonalizer_allowed line 87