CubicMatching.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.cubic_hadamard_row_sum line 11
theorem OAI.MUB6.cubic_hadamard_row_one_count line 15
theorem OAI.MUB6.existsUnique_of_filter_card_one line 26

theorem OAI.MUB6.cubic_hadamard_one_matching line 36

Source documentation

The noninitial entries equal to one form a perfect matching.

theorem cubic_hadamard_one_matching {H : CMatrix} (hH : IsHadamard H)
    (hcube : ∀ i j, H i j ^ 3 = 1)
    (h0row : ∀ j, H 0 j = 1) (h0col : ∀ i, H i 0 = 1) :
    ∃ p : Equiv.Perm (Fin 5), ∀ i j, H i.succ (p j).succ = 1 ↔ i = j := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard

def OAI.MUB6.fixZeroPermutation line 61
Source documentation
Extend a permutation of the five noninitial coordinates by fixing zero.
```
def fixZeroPermutation (p : Equiv.Perm (Fin 5)) : Equiv.Perm Coord where
…
```
Mentions: OAI.MUB6.Coord
theorem OAI.MUB6.fixZeroPermutation_zero line 67
theorem OAI.MUB6.fixZeroPermutation_succ line 70