OAI/Analysis/Quantum/DimensionTen/Mod41Result.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DimensionTen.Mod41.g4 line 8
  2. def OAI.DimensionTen.Mod41.a4 line 10
  3. def OAI.DimensionTen.Mod41.b4 line 12
  4. def OAI.DimensionTen.Mod41.bezout4_t line 14
  5. theorem OAI.DimensionTen.Mod41.bezout4_integer line 16
  6. theorem OAI.DimensionTen.Mod41.bezout4 line 22
  7. abbrev OAI.DimensionTen.Mod41.g10 line 28
  8. def OAI.DimensionTen.Mod41.a10 line 30
  9. def OAI.DimensionTen.Mod41.b10 line 32
  10. def OAI.DimensionTen.Mod41.bezout10_t line 34
  11. theorem OAI.DimensionTen.Mod41.bezout10_integer line 36
  12. theorem OAI.DimensionTen.Mod41.bezout10 line 42
  13. instance OAI.DimensionTen.Mod41.(instance at line 53) line 53
  14. lemma OAI.DimensionTen.Mod41.map_f line 56
  15. lemma OAI.DimensionTen.Mod41.map_u4 line 59
  16. lemma OAI.DimensionTen.Mod41.map_u10 line 61
  17. lemma OAI.DimensionTen.Mod41.horner_monic_degree line 64
  18. lemma OAI.DimensionTen.Mod41.degree_f line 74
  19. lemma OAI.DimensionTen.Mod41.root_f line 92
  20. lemma OAI.DimensionTen.Mod41.divides_twenty line 96
  21. lemma OAI.DimensionTen.Mod41.divides_four line 102
  22. lemma OAI.DimensionTen.Mod41.divides_ten line 107
  23. lemma OAI.DimensionTen.Mod41.coprime_of_equiv line 112
  24. lemma OAI.DimensionTen.Mod41.coprime_remainder_four line 119
  25. lemma OAI.DimensionTen.Mod41.coprime_remainder_ten line 122
  26. lemma OAI.DimensionTen.Mod41.coprime_of_equiv_sub line 125
  27. lemma OAI.DimensionTen.Mod41.coprime_of_equiv_sub_poly line 129
  28. lemma OAI.DimensionTen.Mod41.coprime_four line 133
  29. lemma OAI.DimensionTen.Mod41.coprime_ten line 137
  30. theorem OAI.DimensionTen.Mod41.irreducible_degree_twenty line 143
  31. theorem OAI.DimensionTen.Mod41.irreducible_f_of_card line 164
  32. theorem OAI.DimensionTen.Mod41.irreducible_f line 173