OAI/Analysis/Quantum/DimensionTen/GaloisField.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DimensionTen.Border.K line 11
  2. instance OAI.DimensionTen.Border.(instance at line 12) line 12
  3. instance OAI.DimensionTen.Border.(instance at line 13) line 13
  4. instance OAI.DimensionTen.Border.(instance at line 14) line 14
  5. lemma OAI.DimensionTen.Border.F_map_K line 16
  6. lemma OAI.DimensionTen.Border.F_separable_K line 19
  7. lemma OAI.DimensionTen.Border.F_splits_K line 21
  8. lemma OAI.DimensionTen.Border.roots_card_K line 23
  9. lemma OAI.DimensionTen.Border.aroot_iff_root line 26
  10. def OAI.DimensionTen.Border.embeddingRootEquiv line 36
  11. lemma OAI.DimensionTen.Border.embeddingRootEquiv_apply line 41
  12. lemma OAI.DimensionTen.Border.embeddings_card_K line 44
  13. def OAI.DimensionTen.Border.embeddingsK line 47
  14. def OAI.DimensionTen.Border.complexEmbedding line 50
  15. lemma OAI.DimensionTen.Border.finrank_L line 52
  16. lemma OAI.DimensionTen.Border.embeddings_card_complex line 55
  17. lemma OAI.DimensionTen.Border.complex_embeddings_bijective line 58
  18. def OAI.DimensionTen.Border.embeddingsC line 68
  19. lemma OAI.DimensionTen.Border.galois_permute line 71