OAI/RingTheory/DirectFiniteness/CharacterTwist.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.CharacterTwist.H line 15
  2. def OAI.KaplanskyCounterexample.CharacterTwist.src line 17
  3. def OAI.KaplanskyCounterexample.CharacterTwist.dst line 20
  4. lemma OAI.KaplanskyCounterexample.CharacterTwist.src_injective line 26
  5. lemma OAI.KaplanskyCounterexample.CharacterTwist.dst_injective line 31
  6. abbrev OAI.KaplanskyCounterexample.CharacterTwist.source line 37
  7. abbrev OAI.KaplanskyCounterexample.CharacterTwist.target line 38
  8. def OAI.KaplanskyCounterexample.CharacterTwist.edgeIso line 40
  9. abbrev OAI.KaplanskyCounterexample.CharacterTwist.L line 44
  10. abbrev OAI.KaplanskyCounterexample.CharacterTwist.emb line 45
  11. abbrev OAI.KaplanskyCounterexample.CharacterTwist.τ line 47
  12. lemma OAI.KaplanskyCounterexample.CharacterTwist.emb_injective line 50
  13. lemma OAI.KaplanskyCounterexample.CharacterTwist.conjugacy line 53
  14. lemma OAI.KaplanskyCounterexample.CharacterTwist.central_cyclic line 65
  15. def OAI.KaplanskyCounterexample.CharacterTwist.zHom line 88
  16. def OAI.KaplanskyCounterexample.CharacterTwist.localHom line 89
  17. def OAI.KaplanskyCounterexample.CharacterTwist.e line 91
  18. def OAI.KaplanskyCounterexample.CharacterTwist.P line 92
  19. def OAI.KaplanskyCounterexample.CharacterTwist.Q line 93
  20. def OAI.KaplanskyCounterexample.CharacterTwist.u line 96
  21. def OAI.KaplanskyCounterexample.CharacterTwist.uInv line 98
  22. lemma OAI.KaplanskyCounterexample.CharacterTwist.uInv_mul_u line 102
  23. lemma OAI.KaplanskyCounterexample.CharacterTwist.u_mul_uInv line 105
  24. lemma OAI.KaplanskyCounterexample.CharacterTwist.e_central line 109
  25. lemma OAI.KaplanskyCounterexample.CharacterTwist.cyclic_weight line 113
  26. lemma OAI.KaplanskyCounterexample.CharacterTwist.twisted_single line 128
  27. lemma OAI.KaplanskyCounterexample.CharacterTwist.twisted_average line 136
  28. lemma OAI.KaplanskyCounterexample.CharacterTwist.conjugate_projection line 152