OAI/NumberTheory/SiegelZeros/LocalAlgebra/LocalizedFiltrationLength.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W22.length_filtration_step line 23
2. theorem OAI.SiegelZeros.WeightedTorusJets.W22.length_eq_sum_filtration line 31
3. theorem OAI.SiegelZeros.WeightedTorusJets.W22.module_length_eq_sum_filtration line 45
4. def OAI.SiegelZeros.WeightedTorusJets.W22.subquotientEquivImage line 65
5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.quotient_length_step line 75
6. theorem OAI.SiegelZeros.WeightedTorusJets.W22.quotient_length_eq_sum_and_last line 88
7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.quotient_length_eq_sum_of_last_top line 100
8. theorem OAI.SiegelZeros.WeightedTorusJets.W22.map_colon_singleton_localization line 118
9. def OAI.SiegelZeros.WeightedTorusJets.W22.localizedCyclicFactorEquiv line 130
10. def OAI.SiegelZeros.WeightedTorusJets.W22.primeLocalizedCyclicFactorEquiv line 141
11. theorem OAI.SiegelZeros.WeightedTorusJets.W22.map_ideal_eq_top_of_not_le line 160
12. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localized_prime_factor_length_zero line 168
13. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localized_prime_factor_length_one line 175
14. theorem OAI.SiegelZeros.WeightedTorusJets.W22.prime_not_le_of_ne_minimal line 185
15. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localized_prime_factor_length line 191
16. theorem OAI.SiegelZeros.WeightedTorusJets.W22.local_component_length_eq_prime_factor_count line 206
17. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localized_cyclic_filtration_length line 236