OAI/GroupTheory/FiniteLattice/NormalPreimage.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

Perfect covers, normal-subgroup fences and least perfect preimages.

  1. theorem OAI.FiniteLatticeGap.simple_module_finite line 17
  2. theorem OAI.FiniteLatticeGap.simple_family_commutant_scalar line 35
  3. theorem OAI.FiniteLatticeGap.simple_family_action_surjective line 61
  4. theorem OAI.FiniteLatticeGap.simple_family_degree_sum_le line 85
  5. theorem OAI.FiniteLatticeGap.simple_family_card_le line 94
  6. theorem OAI.FiniteLatticeGap.simple_family_card_le_order line 108
  7. theorem OAI.FiniteLatticeGap.simple_action_surjective line 129
  8. theorem OAI.FiniteLatticeGap.irreducible_degree_sq_le_order line 148
  9. theorem OAI.FiniteLatticeGap.semilinear_fixed_span line 175
  10. theorem OAI.FiniteLatticeGap.semilinear_fixed_basis line 203
  11. theorem OAI.FiniteLatticeGap.matrix_hilbert90 line 218
  12. def OAI.FiniteLatticeGap.semilinearSubrepresentationEquiv line 276
  13. theorem OAI.FiniteLatticeGap.semilinear_isIrreducible line 318
  14. def OAI.FiniteLatticeGap.matrixRepresentation line 326
  15. def OAI.FiniteLatticeGap.matrixTwist line 329
  16. def OAI.FiniteLatticeGap.fieldColumnEquiv line 332
  17. instance OAI.FiniteLatticeGap.matrixTwist_irreducible line 340
  18. theorem OAI.FiniteLatticeGap.matrix_equiv_of_module_equiv line 349
  19. theorem OAI.FiniteLatticeGap.matrix_twist_period line 367
  20. theorem OAI.FiniteLatticeGap.mapMatrix_comp line 389
  21. theorem OAI.FiniteLatticeGap.mapMatrix_id line 392
  22. theorem OAI.FiniteLatticeGap.matrix_twist_period_bound line 395
  23. def OAI.FiniteLatticeGap.matrixFrobEquiv line 431
  24. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_apply line 438
  25. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_smul line 441
  26. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_pow_smul line 447
  27. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_map line 461
  28. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_pow_map line 468
  29. theorem OAI.FiniteLatticeGap.matrixFrobEquiv_pow_finrank line 480
  30. theorem OAI.FiniteLatticeGap.frobenius_matrix_descent line 517
  31. theorem OAI.FiniteLatticeGap.frobenius_lang line 564
  32. theorem OAI.FiniteLatticeGap.prime_power_frobenius_lang line 621
  33. theorem OAI.FiniteLatticeGap.finite_group_field_of_definition line 642
  34. def OAI.FiniteLatticeGap.subrepresentationSurjectiveEquiv line 697
  35. theorem OAI.FiniteLatticeGap.irreducible_of_comp_surjective line 709
  36. theorem OAI.FiniteLatticeGap.irreducible_central_scalar line 720
  37. theorem OAI.FiniteLatticeGap.perfect_det_one line 735
  38. theorem OAI.FiniteLatticeGap.matrix_irreducible_dimension_pos line 742
  39. theorem OAI.FiniteLatticeGap.perfect_irreducible_center_card line 749
  40. theorem OAI.FiniteLatticeGap.perfect_irreducible_image_card line 776
  41. theorem OAI.FiniteLatticeGap.central_quotient_card_le_of_surjective line 794
  42. theorem OAI.FiniteLatticeGap.irreducible_perfect_cover_bounds line 811
  43. structure OAI.FiniteLatticeGap.ChiefNormalSeries line 850
  44. def OAI.FiniteLatticeGap.ChiefNormalSeries.factor line 865
  45. def OAI.FiniteLatticeGap.ChiefNormalSeries.nonabelianCount line 868
  46. def OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.coordPrefix line 877
  47. instance OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.prefix_normal line 887
  48. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.prefix_mono line 893
  49. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.single_mem_coordPrefix line 898
  50. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.prefix_strictMono line 904
  51. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.eval_surjective line 915
  52. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.prefix_saturated line 920
  53. def OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.powerChiefSeries line 958
  54. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.prefix_le_eval_ker line 977
  55. def OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.factorEval line 982
  56. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.factorEval_surjective line 988
  57. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.factorEval_injective line 997
  58. def OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.factorEvalEquiv line 1016
  59. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.powerChiefSeries_factor_perfect line 1020
  60. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.powerChiefSeries_count line 1026
  61. lemma OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.perfect_power line 1039
  62. theorem OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.no_perfect_group_chief_bound line 1046
  63. def OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.PerfectCoverEstimates line 1056
  64. theorem OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.perfectCoverEstimates line 1065
  65. theorem OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.cover_estimates_with_many_chief_layers line 1071
  66. theorem OAI.FiniteLatticeGap.PerfectCoverChiefObstruction.cover_estimates_do_not_imply_five_chief_layers line 1085
  67. def OAI.FiniteLattice.Fenced line 1101
  68. theorem OAI.FiniteLattice.Fenced.not_modular line 1107
  69. theorem OAI.FiniteLattice.Fenced.not_modular_interval line 1118
  70. theorem OAI.FiniteLattice.normal_sup_inf_le line 1138
  71. theorem OAI.FiniteLattice.normal_test line 1147