OAI/NumberTheory/GaussianMoat/ResidueQuotient.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GaussianMoat.multiples line 7
2. lemma OAI.GaussianMoat.twoVectorMap_mul_i line 10
3. lemma OAI.GaussianMoat.mem_multiples line 15
4. lemma OAI.GaussianMoat.multiples_index line 19
5. def OAI.GaussianMoat.gaussianResidue line 27
6. lemma OAI.GaussianMoat.gaussianResidue_eq line 30
7. instance OAI.GaussianMoat.(instance at line 34) line 34
8. instance OAI.GaussianMoat.(instance at line 36) line 36
9. def OAI.GaussianMoat.residueCode line 39
10. lemma OAI.GaussianMoat.residueCode_eq line 43
11. lemma OAI.GaussianMoat.residueCode_sub line 49
12. lemma OAI.GaussianMoat.residueCode_add line 55
13. lemma OAI.GaussianMoat.finite_gaussianResidue line 61
14. lemma OAI.GaussianMoat.residueCode_range_card line 67