`OAI/Analysis/MutuallyUnbiased/Bases/Basic.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MUB6.N6 line 13
Source documentation
Maximum expressed as a supremum of attainable finite family sizes.
```
def N6 : ℕ := sSup {n : ℕ | Attainable n}
…
```
Mentions: OAI.MUB6.Attainable