OAI/RingTheory/DirectFiniteness/FiniteBlock.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteBlock.permAction line 13

   Source documentation

   The coordinate permutation action in the exact finite auxiliary group.

   def permAction : Equiv.Perm m →* MulAut (m → C) where
   …

2. abbrev OAI.KaplanskyCounterexample.FiniteBlock.Auxiliary line 23
3. instance OAI.KaplanskyCounterexample.FiniteBlock.(instance at line 26) line 26
4. def OAI.KaplanskyCounterexample.FiniteBlock.coordinate line 32
5. lemma OAI.KaplanskyCounterexample.FiniteBlock.coordinate_ne line 35
6. def OAI.KaplanskyCounterexample.FiniteBlock.p line 47
7. def OAI.KaplanskyCounterexample.FiniteBlock.permElt line 50
8. lemma OAI.KaplanskyCounterexample.FiniteBlock.permElt_inv_mul line 54
9. lemma OAI.KaplanskyCounterexample.FiniteBlock.permElt_mul_inv line 58
10. lemma OAI.KaplanskyCounterexample.FiniteBlock.p_ne_zero line 62
11. lemma OAI.KaplanskyCounterexample.FiniteBlock.p_idem line 64
12. lemma OAI.KaplanskyCounterexample.FiniteBlock.p_orth line 66
13. lemma OAI.KaplanskyCounterexample.FiniteBlock.translated line 69