OAI/RingTheory/DirectFiniteness/CharacterIdempotents.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.CharacterIdempotents.projector line 12
2. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.sum_character_eq_zero line 15
3. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_mul_single line 30
4. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_mul line 46
5. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_idempotent line 60
6. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_orthogonal line 66
7. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_one_coeff line 79
8. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.projector_ne_zero line 83
9. def OAI.KaplanskyCounterexample.CharacterIdempotents.pushed line 91

   Source documentation

   Transport the character projector along an actual subgroup embedding.

   def pushed (f : A →* G) (χ : A →* Kˣ) : MonoidAlgebra K G :=
   …

10. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_eq_sum line 94
11. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_idempotent line 99
12. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_orthogonal line 105
13. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_ne_zero line 110
14. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_mul_single line 115
15. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.pushed_central line 121
16. lemma OAI.KaplanskyCounterexample.CharacterIdempotents.lift_pushed line 137