OAI/Combinatorics/ThinTrees/RationalMatrix/Squares.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rational squares.

  1. def OAI.AlgorithmicThinTrees.RationalGram.base4Squares line 14
  2. lemma OAI.AlgorithmicThinTrees.RationalGram.base4Squares_sum line 18
  3. lemma OAI.AlgorithmicThinTrees.RationalGram.base4Squares_length line 39
  4. lemma OAI.AlgorithmicThinTrees.RationalGram.base4Squares_entry line 48
  5. def OAI.AlgorithmicThinTrees.RationalGram.scalarFactors line 58
  6. lemma OAI.AlgorithmicThinTrees.RationalGram.scalarFactors_zero line 62
  7. lemma OAI.AlgorithmicThinTrees.RationalGram.scalarFactors_sum line 64
  8. lemma OAI.AlgorithmicThinTrees.RationalGram.product_size line 87
  9. lemma OAI.AlgorithmicThinTrees.RationalGram.scalarFactors_length line 93
  10. lemma OAI.AlgorithmicThinTrees.RationalGram.scalarFactors_parts line 98