OAI/Analysis/Quantum/PPTSquare/GaloisAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CertificateGalois.root_of_product line 27
  2. lemma OAI.CertificateGalois.exists_index_of_product_root line 33
  3. lemma OAI.CertificateGalois.perm_of_integer_roots line 40
  4. lemma OAI.CertificateGalois.map_product_integer_roots line 66
  5. lemma OAI.CertificateGalois.reduction_injective line 76
  6. lemma OAI.CertificateGalois.perm_pow_root line 87
  7. lemma OAI.CertificateGalois.fixed_card_eq_gcd_degree line 94
  8. lemma OAI.CertificateGalois.frobenius_permutation line 138
  9. def OAI.PencilGroup.fixedCount line 202
  10. lemma OAI.PencilGroup.fixed_all line 205
  11. lemma OAI.PencilGroup.fixed_none line 215
  12. lemma OAI.PencilGroup.transitive_of_frob41 line 222
  13. lemma OAI.PencilGroup.swap_of_frob131 line 257
  14. lemma OAI.PencilGroup.cycle_of_frob139 line 267
  15. lemma OAI.PencilGroup.full_symmetric line 286
  16. lemma OAI.IntegralRoots.enumerate_roots line 335
  17. lemma OAI.IntegralRoots.exists_integral_roots line 354
  18. lemma OAI.IntegralRoots.injective_of_squarefree_reduction line 376
  19. def OAI.GaloisAction.permutationImage line 414
  20. lemma OAI.GaloisAction.full_action line 431