OAI/NumberTheory/DirichletL/Detector/GramMobiusLattice.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbeGramCommon.primary_productline 15 - theorem
OAI.SevenEighths.ProbeGramCommon.jointExtension_divisor_latticeline 19