OAI/Combinatorics/ThinTrees/RationalMatrix/Inverse.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rational inverse.

  1. lemma OAI.AlgorithmicThinTrees.RationalInverse.posDef_of_cast line 15
  2. lemma OAI.AlgorithmicThinTrees.RationalInverse.schur_posDef line 32
  3. def OAI.AlgorithmicThinTrees.RationalInverse.liftSolve line 46
  4. lemma OAI.AlgorithmicThinTrees.RationalInverse.liftSolve_correct line 51
  5. def OAI.AlgorithmicThinTrees.RationalInverse.inverse line 84
  6. lemma OAI.AlgorithmicThinTrees.RationalInverse.inverse_mul_correct line 90
  7. lemma OAI.AlgorithmicThinTrees.RationalInverse.inverse_eq line 104
  8. lemma OAI.AlgorithmicThinTrees.RationalInverse.inverse_eq_of_cast line 107