OAI/Algebra/DepthFive/CoefficientMap.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.D5Leaf.mapCoefficients line 12
2. theorem OAI.Problem335.D5Leaf.degree_mapCoefficients line 17
3. theorem OAI.Problem335.D5Leaf.mapCoefficients_id line 22
4. theorem OAI.Problem335.D5Leaf.mapCoefficients_comp line 25
5. def OAI.Problem335.Depth5Circuit.mapCoefficients line 33

   Source documentation

   Pure coefficient relabeling; no algebraic properties are needed for syntactic homogeneity.

   def Depth5Circuit.mapCoefficients {K : Type u} {L : Type v}
       [CommSemiring K] [CommSemiring L] {n : ℕ}
       (f : K → L) (c : Depth5Circuit K n) : Depth5Circuit L n where
   …

   Mentions: OAI.Problem335.Depth5Circuit

6. theorem OAI.Problem335.Depth5Circuit.lowerInputs_mapCoefficients line 72
7. theorem OAI.Problem335.Depth5Circuit.middleInputs_mapCoefficients line 77
8. theorem OAI.Problem335.Depth5Circuit.upperInputs_mapCoefficients line 83
9. theorem OAI.Problem335.Depth5Circuit.outputInputs_mapCoefficients line 88
10. theorem OAI.Problem335.circuitSize_mapCoefficients line 94
11. theorem OAI.Problem335.d5LeafValue_mapCoefficients line 99
12. theorem OAI.Problem335.bottomValue_mapCoefficients line 105
13. theorem OAI.Problem335.lowerValue_mapCoefficients line 112
14. theorem OAI.Problem335.middleValue_mapCoefficients line 119
15. theorem OAI.Problem335.upperValue_mapCoefficients line 126
16. theorem OAI.Problem335.circuitValue_mapCoefficients line 133
17. theorem OAI.Problem335.Depth5Circuit.mapCoefficients_id line 139
18. theorem OAI.Problem335.Depth5Circuit.mapCoefficients_comp line 145