OAI/NumberTheory/DirichletL/Hecke/IdealOperations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SevenEighths.HeckeFamily.(instance at line 10) line 10
2. theorem OAI.SevenEighths.HeckeFamily.idealCoeff_product line 12
3. theorem OAI.SevenEighths.HeckeFamily.exists_primitive_character line 16
4. theorem OAI.SevenEighths.HeckeFamily.exists_primitive_product_character line 29