OAI/Combinatorics/ThinTrees/RationalMatrix/Gram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rational gram.

  1. def OAI.AlgorithmicThinTrees.RationalGram.factorColumns line 14
  2. lemma OAI.AlgorithmicThinTrees.RationalGram.sum_scaled_outer line 19
  3. lemma OAI.AlgorithmicThinTrees.RationalGram.zero_pivot_row line 27
  4. lemma OAI.AlgorithmicThinTrees.RationalGram.factorColumns_correct line 33
  5. def OAI.AlgorithmicThinTrees.RationalGram.factorMatrix line 72
  6. lemma OAI.AlgorithmicThinTrees.RationalGram.factorMatrix_correct line 76
  7. lemma OAI.AlgorithmicThinTrees.RationalGram.trace_parts line 90
  8. lemma OAI.AlgorithmicThinTrees.RationalGram.trace_factor_bounds line 99
  9. lemma OAI.AlgorithmicThinTrees.RationalGram.factorColumns_bounds line 144