OAI/NumberTheory/DirichletL/Hecke/RowNonprincipal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeRowNonprincipal.nonprincipal_of_local_factor line 14
2. theorem OAI.SevenEighths.HeckeRowNonprincipal.actual_row_nonprincipal line 57
3. theorem OAI.SevenEighths.HeckeRowNonprincipal.extract_prime_power line 90
4. theorem OAI.SevenEighths.HeckeRowNonprincipal.principal_row_multiplicity line 116
5. theorem OAI.SevenEighths.HeckeRowNonprincipal.principal_row_fixed_support line 136