OAI/NumberTheory/PrimePackets/RootRelations.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.finite_pretransitive_relation_symmetric line 64
  2. lemma OAI.PrimeDegreePackets.prime_pretransitive_relation_universal line 82
  3. theorem OAI.PrimeDegreePackets.full_invariance_of_prime_root_symmetries line 126
  4. lemma OAI.PrimeDegreePackets.vecMul_mem_pointLattice_rightAction line 146
  5. lemma OAI.PrimeDegreePackets.vecMul_transvection_apply line 158
  6. lemma OAI.PrimeDegreePackets.root_stabilizer_trivial_of_no_coordinate_zero line 168
  7. theorem OAI.PrimeDegreePackets.ae_root_stabilizer_trivial line 198
  8. lemma OAI.PrimeDegreePackets.observationEntropy_map line 212
  9. lemma OAI.PrimeDegreePackets.orbitName_semiconj line 224
  10. lemma OAI.PrimeDegreePackets.observationEntropyRate_map_semiconj line 234
  11. theorem OAI.PrimeDegreePackets.measureEntropy_map_semiconj_le line 249
  12. instance OAI.PrimeDegreePackets.periodSubmodule_addSubgroup_discrete line 267
  13. def OAI.PrimeDegreePackets.orbitQuotientMap line 272
  14. lemma OAI.PrimeDegreePackets.orbitQuotientMap_mk line 283
  15. lemma OAI.PrimeDegreePackets.continuous_orbitQuotientMap line 286
  16. lemma OAI.PrimeDegreePackets.orbitQuotientMap_add line 291
  17. lemma OAI.PrimeDegreePackets.orbitProbability_eq_map_quotient line 300
  18. theorem OAI.PrimeDegreePackets.orbitProbability_entropy_eq_zero line 313
  19. theorem OAI.PrimeDegreePackets.latticePoint_orbitProbability_entropy_eq_zero line 337
  20. lemma OAI.PrimeDegreePackets.measureEntropy_finite_mixture_zero line 351
  21. theorem OAI.PrimeDegreePackets.packetMeasure_entropy_eq_zero line 382
  22. lemma OAI.PrimeDegreePackets.continuous_rootTransvection line 415
  23. lemma OAI.PrimeDegreePackets.root_mul_entry line 427
  24. abbrev OAI.PrimeDegreePackets.RootPivot line 438
  25. abbrev OAI.PrimeDegreePackets.RootSlice line 441
  26. def OAI.PrimeDegreePackets.rootParameter line 443
  27. def OAI.PrimeDegreePackets.rootPivotTranslate line 445
  28. lemma OAI.PrimeDegreePackets.rootParameter_translate line 450
  29. def OAI.PrimeDegreePackets.rootSliceRepresentative line 457
  30. lemma OAI.PrimeDegreePackets.rootSliceRepresentative_translate line 466
  31. lemma OAI.PrimeDegreePackets.continuous_rootParameter line 476
  32. lemma OAI.PrimeDegreePackets.continuous_rootSliceRepresentative line 486
  33. def OAI.PrimeDegreePackets.rootPivotHomeomorph line 494
  34. lemma OAI.PrimeDegreePackets.rootPivotHomeomorph_translate line 520