OAI/NumberTheory/PrimePackets/CharacterPairs.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.integer_squares_sum_one line 123
  2. def OAI.PrimeDegreePackets.characterPair line 151
  3. lemma OAI.PrimeDegreePackets.characterPair_sum_left line 154
  4. lemma OAI.PrimeDegreePackets.characterPair_sum_right line 161
  5. lemma OAI.PrimeDegreePackets.characterPair_mul_left line 168
  6. lemma OAI.PrimeDegreePackets.characterPair_mul_right line 176
  7. lemma OAI.PrimeDegreePackets.characterPair_virtual line 186
  8. theorem OAI.PrimeDegreePackets.heilbronn_degree_one_character line 210
  9. lemma OAI.PrimeDegreePackets.eq_trace_smul_id_of_finrank_one line 251
  10. def OAI.PrimeDegreePackets.degreeOneCharacterHom line 258
  11. def OAI.PrimeDegreePackets.realDegreeOneCharacter line 271
  12. lemma OAI.PrimeDegreePackets.degreeOneCharacter_eq_one_of_fixed_vector line 281
  13. lemma OAI.PrimeDegreePackets.realFiniteCharacter_values line 291
  14. lemma OAI.PrimeDegreePackets.realFiniteCharacter_kernel_index line 303
  15. lemma OAI.PrimeDegreePackets.realFiniteCharacter_trivial_of_odd_index line 322
  16. theorem OAI.PrimeDegreePackets.realGaloisCharacter_trivial_of_odd_degree line 335
  17. theorem OAI.PrimeDegreePackets.heilbronn_principal_of_odd_index line 349
  18. lemma OAI.PrimeDegreePackets.cyclic_degree_one_identity line 400
  19. theorem OAI.PrimeDegreePackets.nonprincipal_realGaloisCharacter_quadratic_subfield line 417
  20. theorem OAI.PrimeDegreePackets.linear_covolume_vector_outside_subspace line 455
  21. theorem OAI.PrimeDegreePackets.linear_covolume_real_basis_in_lattice line 516