OAI/LinearAlgebra/MatrixFields/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate line 15

   Also declared: ComparatorChallenges/MatrixFields.lean:15 (same declaration text).

2. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.eval line 26

   Also declared: ComparatorChallenges/MatrixFields.lean:26 (same declaration text).

3. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Gate.cost line 34

   Also declared: ComparatorChallenges/MatrixFields.lean:34 (same declaration text).

4. inductive OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program line 43

   Also declared: ComparatorChallenges/MatrixFields.lean:43 (same declaration text).

5. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.eval line 51

   Also declared: ComparatorChallenges/MatrixFields.lean:51 (same declaration text).

6. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.cost line 56

   Also declared: ComparatorChallenges/MatrixFields.lean:56 (same declaration text).

7. abbrev OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixInput line 62

   Also declared: ComparatorChallenges/MatrixFields.lean:62 (same declaration text).

8. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.matrixInputs line 64

   Also declared: ComparatorChallenges/MatrixFields.lean:64 (same declaration text).

9. structure OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm line 70

   Also declared: ComparatorChallenges/MatrixFields.lean:70 (same declaration text).

10. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.eval line 79

    Also declared: ComparatorChallenges/MatrixFields.lean:79 (same declaration text).

11. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.Correct line 84

    Also declared: ComparatorChallenges/MatrixFields.lean:84 (same declaration text).

12. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.cost line 87

    Also declared: ComparatorChallenges/MatrixFields.lean:87 (same declaration text).

13. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent line 92

    Source documentation

    Positive slack, one uniform constant, and a correct program at every size.

    Also declared: ComparatorChallenges/MatrixFields.lean:92 (same declaration text).

    def AdmissibleExponent (F : Type*) [Field F] (τ : ℝ) : Prop :=
    …

14. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega line 97

    Also declared: ComparatorChallenges/MatrixFields.lean:97 (same declaration text).