OAI/NumberTheory/DirichletL/Reflection/Independent.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.InverseReflectedPhase.ramifiedBlock_norm line 16
  2. theorem OAI.SevenEighths.InverseReflectedPhase.sourceRowPhase_norm_le_one line 25
  3. theorem OAI.SevenEighths.InverseReflectedPhase.sourceSlotPhase_norm_le_one line 37
  4. theorem OAI.SevenEighths.InverseReflectedPhase.frozenArgument_congr line 50
  5. theorem OAI.SevenEighths.InverseReflectedPhase.frozenCore_congr line 59
  6. theorem OAI.SevenEighths.InverseReflectedPhase.ramifiedBlock_congr line 69
  7. theorem OAI.SevenEighths.InverseReflectedPhase.marked_phases_eq line 78
  8. theorem OAI.SevenEighths.InverseReflectedPhase.marked_sourceColumn_eq line 95
  9. theorem OAI.SevenEighths.InverseReflectedPhase.mixed_coefficient_hybrid_original_exponents line 109