IndexedCircuit.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Problem335.IndexedDepth5Circuit line 12
Source documentation
A depth-five circuit whose gates are indexed by arbitrary finite types. This representation is convenient for products, sums, and path-indexed gates; toDepth5Circuit transports it to the qualified circuit representation.
```
structure IndexedDepth5Circuit (K : Type*) [CommSemiring K] (n : ℕ)
    (L B P M U : Type*) where
…
```
def OAI.Problem335.IndexedDepth5Circuit.toDepth5Circuit line 44
Source documentation
Relabel each finite gate type by Fin without changing any wire or degree.
```
def toDepth5Circuit (c : IndexedDepth5Circuit K n L B P M U) : Depth5Circuit K n where
…
```
Mentions: OAI.Problem335.IndexedDepth5Circuit, OAI.Problem335.Depth5Circuit
theorem OAI.Problem335.IndexedDepth5Circuit.circuitSize_toDepth5Circuit line 84
theorem OAI.Problem335.IndexedDepth5Circuit.outputDegree_toDepth5Circuit line 90