OAI/NumberTheory/PiExponent/Geometry/ConePrimeProperties.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.mapped_minimalPrime_of_prime_extension line 20
2. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.minimalPrime_isHomogeneous line 30
3. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.conePrime_minimal_over_homogenized line 50
4. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.homogenized_span_isHomogeneous line 83
5. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.conePrime_isHomogeneous_of_minimal line 91
6. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime_height_eq line 99
7. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.conePrime_height_eq line 112