OAI/RepresentationTheory/FoulkesHowe/SecondLabels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem346.SecondTransfer.Block line 12

   Source documentation

   Blocks: none is the common vector, some 0 is the fixed first row, and some i.succ is the independent vector in row i.

   abbrev Block (r : ℕ) := Option (Fin (r+1))

2. def OAI.Problem346.SecondTransfer.label line 15

   Source documentation

   In each nonzero row, its first k i factors use the common block.

   def label {r b : ℕ} (k : Fin r → ℕ) (p : Fin (r+1) × Fin b) : Block r :=
   …

   Mentions: OAI.Problem346.SecondTransfer.Block

3. theorem OAI.Problem346.SecondTransfer.label_zero_row line 18
4. theorem OAI.Problem346.SecondTransfer.label_succ_row line 21
5. theorem OAI.Problem346.SecondTransfer.label_zero line 25