OAI/RingTheory/BassTrace/OrbitAreas.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.finsuppRelabel_single line 19
  2. lemma OAI.BassTrace.Sparse.simplexVertices_relabel line 28
  3. lemma OAI.BassTrace.Sparse.sourceInterior_relabel line 36
  4. def OAI.BassTrace.Sparse.simplexPermutation line 47
  5. lemma OAI.BassTrace.Sparse.simplexEnumeration_permutation line 53
  6. lemma OAI.BassTrace.Sparse.simplexCoordinates_relabel line 60
  7. lemma OAI.BassTrace.Sparse.simplexGraph_relabel line 71
  8. lemma OAI.BassTrace.Sparse.originalSimplexArea_relabel line 88
  9. lemma OAI.BassTrace.Sparse.smul_finset_eq_map line 117
  10. abbrev OAI.BassTrace.Sparse.sourceTopAction line 123
  11. lemma OAI.BassTrace.Sparse.sourceTop_stabilizer_eq line 129
  12. lemma OAI.BassTrace.Sparse.finite_sourceTop_stabilizer line 137
  13. def OAI.BassTrace.Sparse.OrbitAreas.representative line 161
  14. lemma OAI.BassTrace.Sparse.OrbitAreas.representative_smul line 163
  15. def OAI.BassTrace.Sparse.OrbitAreas.orbitTimesStabilizer line 166
  16. lemma OAI.BassTrace.Sparse.OrbitAreas.orbitTimesStabilizer_smul line 183
  17. lemma OAI.BassTrace.Sparse.OrbitAreas.sum_orbit_multiplicity line 189
  18. lemma OAI.BassTrace.Sparse.OrbitAreas.normalized_orbit_sum line 201
  19. lemma OAI.BassTrace.Sparse.OrbitAreas.normalized_inverse_orbit_sum line 209
  20. lemma OAI.BassTrace.Sparse.OrbitAreas.normalized_all_orbits line 218
  21. lemma OAI.BassTrace.Sparse.OrbitAreas.finite_finset_stabilizer line 227
  22. def OAI.BassTrace.Sparse.OrbitAreas.orbitActivated line 251
  23. lemma OAI.BassTrace.Sparse.OrbitAreas.measurable_orbitActivated line 255
  24. lemma OAI.BassTrace.Sparse.OrbitAreas.integral_orbitActivated line 263
  25. lemma OAI.BassTrace.Sparse.OrbitAreas.normalized_activated_integral line 271
  26. lemma OAI.BassTrace.Sparse.OrbitAreas.finite_orbit_quotient line 300
  27. def OAI.BassTrace.Sparse.OrbitAreas.orbitReps line 315
  28. lemma OAI.BassTrace.Sparse.OrbitAreas.sum_orbitReps line 319
  29. lemma OAI.BassTrace.Sparse.OrbitAreas.orbitReps_complete line 326