OAI/GroupTheory/FiniteType/Steinberg.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Steinberg.Root line 12
  2. def OAI.Steinberg.letter line 18
  3. inductive OAI.Steinberg.Relation line 21
  4. def OAI.Steinberg.relations line 29
  5. abbrev OAI.Steinberg.Group line 31
  6. def OAI.Steinberg.root line 34
  7. lemma OAI.Steinberg.root_add line 36
  8. lemma OAI.Steinberg.root_commutator line 42
  9. lemma OAI.Steinberg.root_commute line 48
  10. lemma OAI.Steinberg.root_zero line 55
  11. lemma OAI.Steinberg.root_neg line 59
  12. def OAI.Steinberg.lift line 64
  13. lemma OAI.Steinberg.lift_root line 79
  14. theorem OAI.Steinberg.hom_ext line 83
  15. def OAI.Steinberg.map line 89
  16. lemma OAI.Steinberg.map_root line 95
  17. def OAI.Steinberg.matrix line 98
  18. lemma OAI.Steinberg.matrix_root line 103
  19. lemma OAI.Steinberg.matrix_mem line 106
  20. def OAI.Steinberg.pi line 115
  21. lemma OAI.Steinberg.pi_coe line 118
  22. lemma OAI.Steinberg.pi_surjective line 121
  23. structure OAI.CompressedSplittings.BinaryData line 135
  24. def OAI.Steinberg.KernelAnnihilationObligation line 151
  25. lemma OAI.Steinberg.map_id line 155
  26. lemma OAI.Steinberg.map_comp line 162
  27. def OAI.Steinberg.reindex line 170
  28. lemma OAI.Steinberg.reindex_root line 180
  29. lemma OAI.Steinberg.root_commutator_reverse line 184
  30. lemma OAI.Steinberg.opposite_commute_of_support line 190
  31. lemma OAI.Steinberg.roots_commute_orthogonal line 206
  32. lemma OAI.Steinberg.commute_of_roots line 229
  33. lemma OAI.Steinberg.maps_commute_orthogonal line 239
  34. def OAI.Steinberg.orthogonalSum line 252
  35. lemma OAI.Steinberg.orthogonalSum_apply line 259
  36. lemma OAI.Steinberg.map_orthogonalSum line 262