OAI/NumberTheory/DirichletL/Reflection/CubeSlotSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.InverseReflectedPhase.cubeJoined_mark line 16
2. lemma OAI.SevenEighths.InverseReflectedPhase.cubeJoined_completed line 34
3. lemma OAI.SevenEighths.InverseReflectedPhase.cubeJoined_coefficient line 43
4. def OAI.SevenEighths.InverseReflectedPhase.cubeAbsorbedCoefficient line 49
5. lemma OAI.SevenEighths.InverseReflectedPhase.cubeAbsorbedCoefficient_product line 53
6. theorem OAI.SevenEighths.InverseReflectedPhase.original_cube_shifted_tuple_source line 61