OAI/RingTheory/BassTrace/RelativeExponents.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Relative exponents use orbit representatives internally, without assuming an equivariant section.

  1. lemma OAI.BassTrace.RelativeExponents.exists_affine_function line 16
  2. abbrev OAI.BassTrace.RelativeExponents.Positions line 47
  3. lemma OAI.BassTrace.RelativeExponents.centralizer_commutes line 50
  4. def OAI.BassTrace.RelativeExponents.positionHom line 54
  5. def OAI.BassTrace.RelativeExponents.character line 77
  6. lemma OAI.BassTrace.RelativeExponents.character_mul line 80
  7. theorem OAI.BassTrace.RelativeExponents.exists_beta line 87
  8. def OAI.BassTrace.Detector.Vertex line 129
  9. def OAI.BassTrace.Detector.project line 131
  10. def OAI.BassTrace.Detector.sectionLift line 133
  11. lemma OAI.BassTrace.Detector.project_sectionLift line 135
  12. lemma OAI.BassTrace.Detector.project_eq_iff line 138
  13. lemma OAI.BassTrace.Detector.exists_section_power line 151
  14. def OAI.BassTrace.Detector.centralizerAct line 156
  15. lemma OAI.BassTrace.Detector.centralizerAct_project line 165
  16. lemma OAI.BassTrace.Detector.centralizerAct_one line 169
  17. lemma OAI.BassTrace.Detector.centralizerAct_mul line 175
  18. lemma OAI.BassTrace.Detector.centralizerAct_power line 182
  19. lemma OAI.BassTrace.Detector.exists_complex_beta line 187
  20. lemma OAI.BassTrace.Detector.detector_section line 202
  21. lemma OAI.BassTrace.Detector.detector_section_invariant line 217
  22. def OAI.BassTrace.Detector.cosetCocycle line 240
  23. lemma OAI.BassTrace.Detector.cosetCocycle_wedge line 246
  24. lemma OAI.BassTrace.Detector.cosetCocycle_lifts line 255
  25. lemma OAI.BassTrace.Detector.cosetCocycle_closed line 263
  26. lemma OAI.BassTrace.Detector.cosetCocycle_invariant line 272
  27. theorem OAI.BassTrace.Detector.exists_coset_detector line 291
  28. lemma OAI.BassTrace.Detector.square_decomposable line 307
  29. lemma OAI.BassTrace.Detector.nilpotent_binomial line 315
  30. lemma OAI.BassTrace.Detector.factorial_cancel line 334
  31. lemma OAI.BassTrace.Detector.normalized_decomposable_update line 339
  32. lemma OAI.BassTrace.Detector.coordinateVector_minor line 351
  33. lemma OAI.BassTrace.Detector.coordinateVector_indicator line 357
  34. lemma OAI.BassTrace.Detector.pfaffianForm_lift_basis line 361
  35. lemma OAI.BassTrace.Detector.pfaffian_lift_basis line 400