OAI/NumberTheory/DirichletL/PrimeRows/Character.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeHighRowFamily.rowMaskElement line 16
  2. theorem OAI.SevenEighths.ProbeHighRowFamily.rowMaskElement_ne_zero line 18
  3. def OAI.SevenEighths.ProbeHighRowFamily.rawRow line 21
  4. theorem OAI.SevenEighths.ProbeHighRowFamily.rawRow_coeff line 25
  5. theorem OAI.SevenEighths.ProbeHighRowFamily.outside_good_coprime line 33
  6. theorem OAI.SevenEighths.ProbeHighRowFamily.rawRow_prime_outside line 48
  7. def OAI.SevenEighths.ProbeHighRowFamily.rowCharacter line 58
  8. def OAI.SevenEighths.ProbeHighRowFamily.sourceRowCoeff line 61
  9. theorem OAI.SevenEighths.ProbeHighRowFamily.hom_eq_of_primes line 67
  10. theorem OAI.SevenEighths.ProbeHighRowFamily.rowCharacter_coeff line 82
  11. theorem OAI.SevenEighths.ProbeHighRowFamily.target_inverseRow_coeff line 97