ExponentCode.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.MUB6.Certificate.ExponentCode line 9
Source documentation
A finite integer exponent matrix, with its dimensions retained.
```
structure ExponentCode where
…
```
def OAI.MUB6.Certificate.ExponentCode.moment line 16
Source documentation
The interpretation is the actual injective moment defined in Section 2.
```
noncomputable def ExponentCode.moment (H : CMatrix) (A : ExponentCode) : ℝ :=
…
```
Mentions: OAI.MUB6.CMatrix, OAI.MUB6.Certificate.ExponentCode