OAI/Algebra/GroupRing/FreeActionNorm.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.FreeActionNorm.Orbit line 13
  2. def OAI.TorsionFreeZeroDivisors.FreeActionNorm.orbitMap line 14
  3. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.orbit_class line 16
  4. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.orbitMap_bijective line 19
  5. def OAI.TorsionFreeZeroDivisors.FreeActionNorm.orbitEquiv line 32
  6. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.orbitEquiv_apply line 33
  7. def OAI.TorsionFreeZeroDivisors.FreeActionNorm.act line 35
  8. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.act_apply line 37
  9. def OAI.TorsionFreeZeroDivisors.FreeActionNorm.coords line 39
  10. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.coords_coeff line 42
  11. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.coords_act line 44
  12. def OAI.TorsionFreeZeroDivisors.FreeActionNorm.norm line 50
  13. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.coords_norm line 51
  14. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.invariant_norm line 55
  15. lemma OAI.TorsionFreeZeroDivisors.FreeActionNorm.kernel_norm line 75