OAI/Algebra/DepthFive/CoefficientSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.leafCoefficientSet line 12

   Source documentation

   The scalars actually occurring at a leaf.

   def leafCoefficientSet {K : Type u} {n : ℕ} (x : D5Leaf K n) : Finset K := by
   …

   Mentions: OAI.Problem335.D5Leaf

2. def OAI.Problem335.circuitCoefficientSet line 19

   Source documentation

   All coefficients occurring in a circuit, including weighted wires.

   def circuitCoefficientSet {K : Type u} [CommSemiring K] {n : ℕ}
       (c : Depth5Circuit K n) : Finset K := by
   …

   Mentions: OAI.Problem335.Depth5Circuit

3. lemma OAI.Problem335.leaf_scalar_mem_coefficientSet line 27
4. lemma OAI.Problem335.bottom_coeff_mem_coefficientSet line 35
5. lemma OAI.Problem335.middle_coeff_mem_coefficientSet line 44
6. lemma OAI.Problem335.output_coeff_mem_coefficientSet line 53
7. def OAI.Problem335.circuitCoefficientField line 62

   Source documentation

   The subfield generated by the finitely many coefficients of a circuit.

   def circuitCoefficientField {K : Type u} [Field K] {n : ℕ}
       (c : Depth5Circuit K n) : Subfield K :=
   …

   Mentions: OAI.Problem335.Depth5Circuit

8. lemma OAI.Problem335.leaf_scalar_mem line 66
9. lemma OAI.Problem335.bottom_coeff_mem line 71
10. lemma OAI.Problem335.middle_coeff_mem line 76
11. lemma OAI.Problem335.output_coeff_mem line 81
12. instance OAI.Problem335.circuitCoefficientField_countable line 86