OAI/NumberTheory/DirichletL/Detector/GramPrimaryLattice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbeGramCommon.PrimaryElement line 15
2. def OAI.SevenEighths.ProbeGramCommon.primaryIdealEquiv line 17
3. lemma OAI.SevenEighths.ProbeGramCommon.primaryCoefficient_nonzero_supported line 24
4. lemma OAI.SevenEighths.ProbeGramCommon.primary_factor_right line 36
5. lemma OAI.SevenEighths.ProbeGramCommon.primaryCoefficient_residual line 40
6. theorem OAI.SevenEighths.ProbeGramCommon.primary_ideal_tsum line 50
7. theorem OAI.SevenEighths.ProbeGramCommon.primary_ideal_pair_tsum line 58