OAI/NumberTheory/DirichletL/Reflection/MarkedJoined.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.InverseReflectedPhase.joined_whole_prime_mark line 12
  2. theorem OAI.SevenEighths.InverseReflectedPhase.actual_marked_row_eq_joined line 26
  3. lemma OAI.SevenEighths.InverseReflectedPhase.joined_free_pairwise line 45