OAI/NumberTheory/PrimePackets/RayContinuation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.EvenRayCharacter.IsNonprincipal line 17
  2. lemma OAI.PrimeDegreePackets.EvenRayCharacter.conjugate_isNonprincipal line 22
  3. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classCharacter_ne_one_of_nonprincipal line 35
  4. def OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued line 49
  5. theorem OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_entire line 53
  6. theorem OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_eq_dirichlet line 61
  7. lemma OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_ne_zero_right line 71
  8. lemma OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_ne_zero line 78
  9. theorem OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_finite_nonnegative_order line 87
  10. theorem OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_conjugation line 104
  11. theorem OAI.PrimeDegreePackets.EvenRayCharacter.nonprincipalContinued_order_conjugation line 122