OAI/NumberTheory/SiegelZeros/Hilbert/HomogeneousComponentLength.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W22.homogeneous_colon_singleton line 22
2. theorem OAI.SiegelZeros.WeightedTorusJets.W22.exists_homogeneous_prime_colon line 36
3. def OAI.SiegelZeros.WeightedTorusJets.W22.HomogeneousPrimeStep line 91
4. theorem OAI.SiegelZeros.WeightedTorusJets.W22.HomogeneousPrimeStep.homogeneous line 97
5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.HomogeneousPrimeStep.lt line 108
6. theorem OAI.SiegelZeros.WeightedTorusJets.W22.HomogeneousPrimeStep.isQuotientEquivQuotientPrime line 119
7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.exists_homogeneous_prime_filtration line 125
8. theorem OAI.SiegelZeros.WeightedTorusJets.W22.exists_homogeneous_cyclic_filtration_nat line 161
9. theorem OAI.SiegelZeros.WeightedTorusJets.W22.exists_homogeneous_component_length_count line 214