OAI/Analysis/MutuallyUnbiased/MixedSemantics/Code.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MUB6.Certificate.MixedSemantics.Code line 9

   Source documentation

   A finite integer mixed-moment descriptor, retaining every index size.

   structure Code where
   …

2. instance OAI.MUB6.Certificate.MixedSemantics.(instance at line 16) line 16
3. abbrev OAI.MUB6.Certificate.MixedSemantics.Master line 20

   Source documentation

   Pair coordinates and all elementary mixed nodes share one ambient space. The numerical certificate is reindexed into this space separately.

   abbrev Master := Fin 909 ⊕ Fin 5502
   …