OAI/NumberTheory/DirichletL/Reflection/MarkedRow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseReflectedPhase.markedCompletedT_twist_congr_primary line 13
2. theorem OAI.SevenEighths.InverseReflectedPhase.actual_marked_row_fixed_factor line 23
3. def OAI.SevenEighths.InverseReflectedPhase.freePrimeFamily line 34
4. def OAI.SevenEighths.InverseReflectedPhase.markedSumSlots line 39
5. lemma OAI.SevenEighths.InverseReflectedPhase.actual_sextic_power_congr line 42
6. lemma OAI.SevenEighths.InverseReflectedPhase.unmarked_sum_twist line 49
7. theorem OAI.SevenEighths.InverseReflectedPhase.free_row_eq_joined_unmarked line 68