OAI/NumberTheory/DirichletL/PrimeRows/Principal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbeHighRowFamily.rawRow_elementCoeff line 16
  2. lemma OAI.SevenEighths.ProbeHighRowFamily.rowCharacter_principal_iff line 23
  3. lemma OAI.SevenEighths.ProbeHighRowFamily.supported_coprime_row_fixed line 27
  4. theorem OAI.SevenEighths.ProbeHighRowFamily.rawRow_principal_supported_isUnit line 48
  5. lemma OAI.SevenEighths.ProbeHighRowFamily.idealCoeff_principal_eq_one line 74
  6. theorem OAI.SevenEighths.ProbeHighRowFamily.rowCharacter_unit_nonprincipal line 84
  7. theorem OAI.SevenEighths.ProbeHighRowFamily.rowCharacter_principal_supported_eq_one line 100