OAI/GroupTheory/ArithmeticGerms/Stabilizers.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Full arithmetic germ stabilizers and finite orbits.

  1. class OAI.ArithmeticGerms.ICC line 14
  2. lemma OAI.ArithmeticGerms.finiteIndex_comap line 20
  3. lemma OAI.ArithmeticGerms.finiteIndex_map line 26
  4. lemma OAI.ArithmeticGerms.finiteIndex_image_of_relIndex line 33
  5. theorem OAI.ArithmeticGerms.eq_one_of_centralizes_finiteIndex line 50
  6. def OAI.ArithmeticGerms.VirtualGraph.toDomain line 84
  7. def OAI.ArithmeticGerms.VirtualGraph.toCodomain line 89
  8. def OAI.ArithmeticGerms.VirtualGraph.iso line 94
  9. lemma OAI.ArithmeticGerms.VirtualGraph.pair_mem_graph line 97
  10. lemma OAI.ArithmeticGerms.VirtualGraph.finiteRelIndex_of_fst line 106
  11. lemma OAI.ArithmeticGerms.VirtualGraph.commensurable_of_le line 124
  12. def OAI.ArithmeticGerms.VirtualGraph.restriction line 129
  13. theorem OAI.ArithmeticGerms.VirtualGraph.commensurable_iff_common_restriction line 145
  14. lemma OAI.ArithmeticGerms.VirtualGraph.iso_extends line 156
  15. def OAI.ArithmeticGerms.VirtualGraph.ofEquiv line 164
  16. def OAI.ArithmeticGerms.VirtualGraph.conjugate line 188
  17. lemma OAI.ArithmeticGerms.VirtualGraph.conjugate_graph line 217
  18. instance OAI.ArithmeticGerms.VirtualGraph.(instance at line 220) line 220
  19. lemma OAI.ArithmeticGerms.VirtualGraph.smul_graph line 231
  20. def OAI.ArithmeticGerms.VirtualGraph.fullSubgroup line 234
  21. lemma OAI.ArithmeticGerms.VirtualGraph.graph_le_fullSubgroup line 237
  22. lemma OAI.ArithmeticGerms.VirtualGraph.snd_eq_one_of_mem_fullSubgroup line 242
  23. lemma OAI.ArithmeticGerms.VirtualGraph.fst_eq_one_of_mem_fullSubgroup line 266
  24. def OAI.ArithmeticGerms.VirtualGraph.full line 290
  25. lemma OAI.ArithmeticGerms.VirtualGraph.commensurable_full line 305
  26. lemma OAI.ArithmeticGerms.VirtualGraph.finiteIndex_in_full line 309
  27. def OAI.ArithmeticGerms.germSetoid line 315
  28. def OAI.ArithmeticGerms.Germ line 319
  29. def OAI.ArithmeticGerms.Germ.mk line 324
  30. lemma OAI.ArithmeticGerms.Germ.induction_on line 327
  31. lemma OAI.ArithmeticGerms.Germ.mk_eq_mk_iff line 330
  32. instance OAI.ArithmeticGerms.Germ.(instance at line 333) line 333
  33. lemma OAI.ArithmeticGerms.Germ.smul_mk line 345
  34. def OAI.ArithmeticGerms.Germ.full line 350
  35. lemma OAI.ArithmeticGerms.Germ.full_mk line 355
  36. theorem OAI.ArithmeticGerms.Germ.full_graph_eq_stabilizer line 357
  37. lemma OAI.ArithmeticGerms.Germ.mk_full line 364
  38. lemma OAI.ArithmeticGerms.Germ.mem_full_iff line 368
  39. theorem OAI.ArithmeticGerms.Germ.representative_in_full line 372
  40. theorem OAI.ArithmeticGerms.Germ.eq_mk_of_fixed_by_finiteIndex line 376
  41. theorem OAI.ArithmeticGerms.Germ.eq_of_fixed_by_finiteIndex line 387
  42. theorem OAI.ArithmeticGerms.Germ.finite_orbit_iff_eq_mk line 397
  43. theorem OAI.ArithmeticGerms.Germ.finite_orbit_iff line 422
  44. def OAI.ArithmeticGerms.Germ.inner line 429
  45. theorem OAI.ArithmeticGerms.Germ.inner_injective line 431
  46. theorem OAI.ArithmeticGerms.full_stabilizers_and_finite_orbit_test line 450