OAI/Algebra/FormulaHitting/Model.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.NCHitting.Word line 8

   Also declared: ComparatorChallenges/FormulaHitting.lean:8 (same declaration text).

2. abbrev OAI.NCHitting.WordSeries line 9

   Also declared: ComparatorChallenges/FormulaHitting.lean:9 (same declaration text).

3. def OAI.NCHitting.convolution line 11

   Also declared: ComparatorChallenges/FormulaHitting.lean:11 (same declaration text).

4. inductive OAI.NCHitting.Formula line 16

   Also declared: ComparatorChallenges/FormulaHitting.lean:16 (same declaration text).

5. def OAI.NCHitting.Formula.size line 24

   Also declared: ComparatorChallenges/FormulaHitting.lean:24 (same declaration text).

6. def OAI.NCHitting.Formula.coeff line 30

   Also declared: ComparatorChallenges/FormulaHitting.lean:30 (same declaration text).

7. def OAI.NCHitting.Formula.eval line 37

   Also declared: ComparatorChallenges/FormulaHitting.lean:37 (same declaration text).

8. def OAI.NCHitting.dimension line 46

   Also declared: ComparatorChallenges/FormulaHitting.lean:46 (same declaration text).

9. def OAI.NCHitting.matrixEntry line 48

   Also declared: ComparatorChallenges/FormulaHitting.lean:48 (same declaration text).

10. def OAI.NCHitting.generator line 52

    Distinct definitions of this name: ComparatorChallenges/FormulaHitting.lean:52 (same statement text; different proof or body). Qualify references as OAI.NCHitting.generator@path.