OAI/NumberTheory/DirichletL/Detector/GramFiniteGcd.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbeGramCommon.supportedIdealProduct_injectiveline 11 - def
OAI.SevenEighths.ProbeGramCommon.commonPoolline 16 - def
OAI.SevenEighths.ProbeGramCommon.commonColumnsline 18 - lemma
OAI.SevenEighths.ProbeGramCommon.commonColumns_memline 20 - def
OAI.SevenEighths.ProbeGramCommon.commonTriplesline 23 - theorem
OAI.SevenEighths.ProbeGramCommon.finite_pair_gcdline 26