Words.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactFourier.IsMonomial line 8
Source documentation
A permutation matrix times an invertible diagonal matrix, literally P D.
```
def IsMonomial {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) : Prop :=
…
```

def OAI.ExactFourier.embeddedCall line 13

Source documentation

A call on an ordered tuple of distinct coordinates; all other values are fixed.

noncomputable def embeddedCall {q w : ℕ} (A : Matrix (Fin q) (Fin q) ℂ)
    (e : Fin q ↪ Fin w) : Matrix (Fin w) (Fin w) ℂ := by
…

inductive OAI.ExactFourier.WordStep line 20
Source documentation
Only forward calls to the specified A are allowed.
```
inductive WordStep {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (w : ℕ) where
…
```
def OAI.ExactFourier.WordStep.matrix line 24
def OAI.ExactFourier.WordStep.calls line 29
def OAI.ExactFourier.wordMatrix line 34
Source documentation
Stored chronologically, so a new step left-multiplies earlier steps.
```
noncomputable def wordMatrix {q w : ℕ} {A : Matrix (Fin q) (Fin q) ℂ}
    (W : List (WordStep A w)) : Matrix (Fin w) (Fin w) ℂ :=
…
```
Mentions: OAI.ExactFourier.WordStep
def OAI.ExactFourier.wordCalls line 38
def OAI.ExactFourier.tensorCoordinates line 42
Source documentation
A fixed coordinate relabeling of the ordinary Kronecker tensor power.
```
noncomputable def tensorCoordinates (q b : ℕ) : Fin (q ^ b) ≃ (Fin b → Fin q) := by
…
```
def OAI.ExactFourier.tensorPower line 47
def OAI.ExactFourier.FiniteWinStatement line 51