OAI/RepresentationTheory/Saxl/PositionTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.joinPositions line 12

   Source comment

   Concatenation of words on independent position blocks.

   def joinPositions {n a b d : ℕ} (e : Fin n ≃ Fin a ⊕ Fin b)
       (x : Fin a → Fin d) (y : Fin b → Fin d) : Fin n → Fin d :=
   …

2. lemma OAI.Saxl.leftWord_join line 16
3. lemma OAI.Saxl.rightWord_join line 21
4. lemma OAI.Saxl.joinPositions_parts line 26
5. def OAI.Saxl.positionUncurry line 32
6. def OAI.Saxl.positionTensor line 41
7. lemma OAI.Saxl.positionTensor_tmul line 45
8. lemma OAI.Saxl.positionProduct_equivariant line 52
9. lemma OAI.Saxl.positionTensor_equivariant line 68
10. lemma OAI.Saxl.product_mem_cyclic line 77