OAI/Algebra/BogomolovPop/PowerCompletion.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative power completions, integral characters and Frobenius endomorphisms.

  1. def OAI.BogomolovPop.powerSubgroup line 13
  2. abbrev OAI.BogomolovPop.PowerClass line 16
  3. def OAI.BogomolovPop.PowerClass.mk line 21
  4. theorem OAI.BogomolovPop.PowerClass.mk_eq_one line 23
  5. def OAI.BogomolovPop.PowerClass.map line 26
  6. theorem OAI.BogomolovPop.PowerClass.map_mk line 31
  7. theorem OAI.BogomolovPop.PowerClass.map_comp line 34
  8. theorem OAI.BogomolovPop.PowerClass.map_id line 39
  9. def OAI.BogomolovPop.PowerClass.reduce line 43
  10. theorem OAI.BogomolovPop.PowerClass.reduce_mk line 49
  11. theorem OAI.BogomolovPop.PowerClass.map_reduce line 52
  12. def OAI.BogomolovPop.powerCompletionGroup line 58
  13. abbrev OAI.BogomolovPop.PowerCompletion line 72
  14. theorem OAI.BogomolovPop.PowerCompletion.ext line 77
  15. def OAI.BogomolovPop.PowerCompletion.of line 80
  16. def OAI.BogomolovPop.PowerCompletion.map line 83
  17. theorem OAI.BogomolovPop.PowerCompletion.map_val line 90
  18. theorem OAI.BogomolovPop.PowerCompletion.map_of line 93
  19. theorem OAI.BogomolovPop.PowerCompletion.map_comp line 96
  20. theorem OAI.BogomolovPop.PowerCompletion.map_injective line 101
  21. theorem OAI.BogomolovPop.PowerCompletion.range_iff line 110
  22. theorem OAI.BogomolovPop.PowerClass.pow_eq_one line 136
  23. theorem OAI.BogomolovPop.PowerCompletion.pow_ell_eq_one line 145
  24. theorem OAI.BogomolovPop.PowerCompletion.pow_eq_one line 165
  25. theorem OAI.BogomolovPop.field_torsion_divisible line 194
  26. theorem OAI.BogomolovPop.field_completion_pow_eq_one line 214
  27. def OAI.BogomolovPop.inclusionUnits line 219
  28. def OAI.BogomolovPop.normUnits line 222
  29. theorem OAI.BogomolovPop.completion_norm_inclusion line 225
  30. theorem OAI.BogomolovPop.finite_extension_completion_injective line 244
  31. def OAI.BogomolovPop.RelativelyAlgebraicallyClosed line 260
  32. theorem OAI.BogomolovPop.kummer_level_injective line 263
  33. theorem OAI.BogomolovPop.relatively_closed_completion_saturated line 285
  34. theorem OAI.BogomolovPop.completion_coprime_saturated line 335
  35. theorem OAI.BogomolovPop.relatively_closed_completion_nat_saturated line 357
  36. theorem OAI.BogomolovPop.independent_powerClass_injective line 384
  37. theorem OAI.BogomolovPop.independent_completion_injective line 414
  38. theorem OAI.BogomolovPop.inclusionUnits_comp line 428
  39. theorem OAI.BogomolovPop.fg_extension_completion_injective line 434
  40. def OAI.BogomolovPop.rationalDegree line 457
  41. lemma OAI.BogomolovPop.rational_variable_completion_ne_one line 462
  42. lemma OAI.BogomolovPop.transcendental_completion_ne_one line 480
  43. theorem OAI.BogomolovPop.field_completion_kernel_constants line 503
  44. def OAI.BogomolovPop.polynomialTotalDegree line 543
  45. lemma OAI.BogomolovPop.polynomialTotalDegree_unit line 559
  46. def OAI.BogomolovPop.fractionTotalDegree line 564
  47. lemma OAI.BogomolovPop.fractionTotalDegree_algebraMap line 569
  48. def OAI.BogomolovPop.fractionDegreeUnits line 573
  49. lemma OAI.BogomolovPop.fractionDegreeUnits_X line 578
  50. theorem OAI.BogomolovPop.transcendental_integer_character line 595
  51. def OAI.BogomolovPop.KummerScalarLevels line 650
  52. lemma OAI.BogomolovPop.integer_character_scalar line 654
  53. theorem OAI.BogomolovPop.kummer_scalar_rational line 679
  54. lemma OAI.BogomolovPop.exponent_eq_of_zmod line 698
  55. theorem OAI.BogomolovPop.kummer_scalar_power_constants line 706
  56. lemma OAI.BogomolovPop.cyclic_character_scalar_integer line 730
  57. theorem OAI.BogomolovPop.kummer_endomorphism_scalar_integer line 757
  58. def OAI.BogomolovPop.IntegerPowerModuloConstants line 772
  59. lemma OAI.BogomolovPop.transcendental_ne_zero line 778
  60. lemma OAI.BogomolovPop.transcendental_add_constant line 783
  61. lemma OAI.BogomolovPop.integer_power_shift_nonneg line 790
  62. lemma OAI.BogomolovPop.positive_power_shift line 813
  63. lemma OAI.BogomolovPop.power_relation_shift line 828
  64. lemma OAI.BogomolovPop.power_endomorphism_transcendental line 842
  65. lemma OAI.BogomolovPop.polynomial_power_prime line 852
  66. lemma OAI.BogomolovPop.algebraic_is_constant line 881
  67. lemma OAI.BogomolovPop.power_endomorphism_constants line 889
  68. theorem OAI.BogomolovPop.integer_power_endomorphism_rigid line 910
  69. theorem OAI.BogomolovPop.kummer_endomorphism_frobenius line 935