OAI/NumberTheory/DirichletL/Hecke/Conjugation.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.HeckeFamily.idealCoeff_inverse_conjline 11 - theorem
OAI.SevenEighths.HeckeFamily.idealTerm_inverse_conjline 22 - theorem
OAI.SevenEighths.HeckeFamily.LFunction_inverse_conjline 36