OAI/GroupTheory/FiniteType/TorusAction.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorusAction.basePerm line 17
  2. lemma OAI.TorusAction.basePerm_apply line 21
  3. lemma OAI.TorusAction.basePerm_of line 24
  4. lemma OAI.TorusAction.base_shift line 28
  5. lemma OAI.TorusAction.inverse_shift_base line 34
  6. def OAI.TorusAction.representation line 40
  7. lemma OAI.TorusAction.representation_embed line 44
  8. lemma OAI.TorusAction.representation_stable line 48
  9. lemma OAI.TorusAction.basePerm_stage line 55
  10. lemma OAI.TorusAction.shift_pow_stage line 65
  11. lemma OAI.TorusAction.representation_injective line 73
  12. lemma OAI.TorusAction.tuple_transitivity line 101
  13. instance OAI.StageConstruction.columnMulAction line 133
  14. lemma OAI.StageConstruction.smul_eq_action line 135
  15. instance OAI.StageConstruction.columnFaithful line 137
  16. abbrev OAI.StageConstruction.LimitGroup line 151
  17. abbrev OAI.StageConstruction.LimitPoints line 152
  18. def OAI.StageConstruction.limitRepresentation line 154
  19. lemma OAI.StageConstruction.limitRepresentation_injective line 160
  20. lemma OAI.StageConstruction.limit_tuple_transitivity line 170
  21. lemma OAI.StageConstruction.limitPoints_countable line 179
  22. lemma OAI.StageConstruction.stagePoints_infinite line 184
  23. lemma OAI.StageConstruction.limitPoints_infinite line 192
  24. def OAI.Steinberg.coefficients line 206
  25. lemma OAI.Steinberg.mem_coefficients line 224
  26. def OAI.Steinberg.rootSet line 228
  27. lemma OAI.Steinberg.root_mem_normalClosure_span line 232
  28. lemma OAI.Steinberg.map_surjective line 243
  29. lemma OAI.Steinberg.normalClosure_kernel_le line 255
  30. lemma OAI.Steinberg.root_sub line 267
  31. lemma OAI.Steinberg.root_image_eq line 271
  32. def OAI.Steinberg.descendCoefficients line 279
  33. lemma OAI.Steinberg.descendCoefficients_comp line 297
  34. theorem OAI.Steinberg.ker_map line 307
  35. theorem OAI.Steinberg.ker_map_span line 325
  36. lemma OAI.Steinberg.rootSet_finite line 342
  37. theorem OAI.Steinberg.finitelyPresented_quotient line 355
  38. def OAI.Steinberg.coefficientSubring line 362
  39. lemma OAI.Steinberg.closure_roots_eq_top line 377
  40. theorem OAI.Steinberg.finitelyGenerated line 394