FirstLabels.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem346.FirstBlock line 9
Source documentation
Blocks for the first transfer: none is x, some none is t, and some (some j) is the j-th common product factor.
```
abbrev FirstBlock (m : ℕ) := Option (Option (Fin m))
```
def OAI.Problem346.firstLabel line 12
Source documentation
The slot labels after transferring the first k factors out of the t block.
```
def firstLabel (r m k : ℕ) (p : Fin (r+1) × Fin (r+m)) : FirstBlock m :=
…
```
Mentions: OAI.Problem346.FirstBlock
theorem OAI.Problem346.firstLabel_zero_row line 18
theorem OAI.Problem346.firstLabel_succ_row line 23
theorem OAI.Problem346.firstLabel_initial_zero_row line 28