OAI/NumberTheory/SiegelZeros/LocalAlgebra/RegularSequenceSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W20.prefixIdeal_succ line 15
2. theorem OAI.SiegelZeros.W20.regular_next_mod_prefix line 22
3. theorem OAI.SiegelZeros.W20.prefixIdeal_zero line 35
4. theorem OAI.SiegelZeros.W20.prefixIdeal_length line 38
5. theorem OAI.SiegelZeros.W20.prefixIdeal_homogeneous line 51
6. theorem OAI.SiegelZeros.W20.regular_prefix_hilbert_recurrence line 61
7. def OAI.SiegelZeros.WeightedTorusJets.W64.degreeAt line 97
8. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_prefix_series line 100
9. theorem OAI.SiegelZeros.WeightedTorusJets.W64.degree_factors_mul_invOneSubPow line 127
10. theorem OAI.SiegelZeros.WeightedTorusJets.W64.regular_sequence_series_geometric line 142