OAI/NumberTheory/DirichletL/Hecke/InverseAmplificationFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.HeckeInverseAmplification.NonzeroElement line 10
2. structure OAI.SevenEighths.HeckeInverseAmplification.RowData line 12
3. def OAI.SevenEighths.HeckeInverseAmplification.RowData.character line 21
4. theorem OAI.SevenEighths.HeckeInverseAmplification.RowData.character_spec line 25
5. def OAI.SevenEighths.HeckeInverseAmplification.amplifiedElement line 31
6. theorem OAI.SevenEighths.HeckeInverseAmplification.RowData.amplified_prime_mask line 35
7. theorem OAI.SevenEighths.HeckeInverseAmplification.RowData.prime_column line 46
8. theorem OAI.SevenEighths.HeckeInverseAmplification.RowData.prime_energy line 57