OAI/RepresentationTheory/AlperinWeights/Brauer.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Brauer projection and foundations for blockwise Alperin weights.

  1. abbrev OAI.BlockwiseAW.AlgebraicIntegers line 9
  2. lemma OAI.BlockwiseAW.exists_integer_reduction line 11
  3. def OAI.BlockwiseAW.integerReduction line 51
  4. theorem OAI.BlockwiseAW.invariant_sum_eq_fixedPoint_sum line 60
  5. abbrev OAI.BlockwiseAW.Center line 112
  6. theorem OAI.BlockwiseAW.mem_center_iff_coeff_conj line 115
  7. def OAI.BlockwiseAW.coefficientRestriction line 131
  8. theorem OAI.BlockwiseAW.coefficientRestriction_coeff line 137
  9. theorem OAI.BlockwiseAW.coefficientRestriction_mem_center line 141
  10. def OAI.BlockwiseAW.centerRestriction line 148
  11. def OAI.BlockwiseAW.classSum line 154
  12. def OAI.BlockwiseAW.conjugationInvariants line 172
  13. theorem OAI.BlockwiseAW.mem_conjugationInvariants_iff line 176
  14. theorem OAI.BlockwiseAW.coeff_mul_sum line 189
  15. theorem OAI.BlockwiseAW.coefficientRestriction_one line 195
  16. theorem OAI.BlockwiseAW.coefficientRestriction_mul_of_invariant line 203
  17. def OAI.BlockwiseAW.brauerHom line 247
  18. theorem OAI.BlockwiseAW.finite_simple_quotients line 261
  19. structure OAI.BlockwiseAW.Block line 301
  20. structure OAI.BlockwiseAW.SimpleRepresentation line 308
  21. theorem OAI.BlockwiseAW.irreducible_moduleFinite line 315
  22. theorem OAI.BlockwiseAW.exists_coordinate_simple line 322
  23. def OAI.BlockwiseAW.SimpleRepresentation.BelongsTo line 340
  24. def OAI.BlockwiseAW.simpleModuleSetoid line 343
  25. def OAI.BlockwiseAW.SimpleModuleClasses line 352
  26. instance OAI.BlockwiseAW.finiteSimpleModuleClasses line 354
  27. def OAI.BlockwiseAW.l line 384
  28. def OAI.BlockwiseAW.IsCentralCharacter line 386
  29. def OAI.BlockwiseAW.OrdinaryCharacter line 393
  30. def OAI.BlockwiseAW.OrdinaryCharacter.degree line 400
  31. def OAI.BlockwiseAW.OrdinaryCharacter.affording line 402
  32. instance OAI.BlockwiseAW.OrdinaryCharacter.affording_irreducible line 405
  33. theorem OAI.BlockwiseAW.OrdinaryCharacter.affording_character line 408
  34. theorem OAI.BlockwiseAW.OrdinaryCharacter.apply_conj line 411
  35. theorem OAI.BlockwiseAW.OrdinaryCharacter.degree_spec line 416
  36. theorem OAI.BlockwiseAW.OrdinaryCharacter.degree_pos line 421
  37. theorem OAI.BlockwiseAW.OrdinaryCharacter.orthogonality line 428
  38. theorem OAI.BlockwiseAW.OrdinaryCharacter.linearIndependent line 441
  39. instance OAI.BlockwiseAW.OrdinaryCharacter.finite line 457
  40. def OAI.BlockwiseAW.pPart line 461
  41. abbrev OAI.BlockwiseAW.Normalizer line 463
  42. abbrev OAI.BlockwiseAW.NormalizerQuotient line 466
  43. structure OAI.BlockwiseAW.Weight line 469
  44. def OAI.BlockwiseAW.Weight.inflatedCharacter line 478
  45. def OAI.BlockwiseAW.Weight.extendedCharacter line 481
  46. def OAI.BlockwiseAW.Weight.IsConjugate line 485
  47. theorem OAI.BlockwiseAW.Weight.isConjugate_refl line 490
  48. theorem OAI.BlockwiseAW.Weight.isConjugate_symm line 493
  49. theorem OAI.BlockwiseAW.Weight.isConjugate_trans line 502
  50. instance OAI.BlockwiseAW.Weight.finite line 512
  51. def OAI.BlockwiseAW.Weight.conjugacySetoid line 521
  52. def OAI.BlockwiseAW.IsOrdinaryReduction line 530
  53. def OAI.BlockwiseAW.AssignedTo line 536
  54. def OAI.BlockwiseAW.W line 545
  55. instance OAI.BlockwiseAW.finiteW line 549