OAI/NumberTheory/DirichletL/Reflection/CubeSlotChoices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.cubeDivList line 12
2. def OAI.SevenEighths.InverseReflectedPhase.cubeAwayList line 13
3. def OAI.SevenEighths.InverseReflectedPhase.cubeChoiceActive line 14
4. abbrev OAI.SevenEighths.InverseReflectedPhase.CubeSlotChoices line 17
5. def OAI.SevenEighths.InverseReflectedPhase.cubeChoicesJoin line 20
6. lemma OAI.SevenEighths.InverseReflectedPhase.cubeChoicesJoin_label line 25
7. lemma OAI.SevenEighths.InverseReflectedPhase.cubeChoicesJoin_injective line 46
8. lemma OAI.SevenEighths.InverseReflectedPhase.cubeChoicesJoin_surjective line 64
9. def OAI.SevenEighths.InverseReflectedPhase.cubeSlotChoiceEquiv line 80