OAI/Combinatorics/ThinTrees/Pencil/AffinePencil.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Affine pencil.

  1. abbrev OAI.AlgorithmicThinTrees.RationalForms.Affine line 14
  2. def OAI.AlgorithmicThinTrees.RationalForms.Affine.cst line 19
  3. def OAI.AlgorithmicThinTrees.RationalForms.Affine.coord line 20
  4. def OAI.AlgorithmicThinTrees.RationalForms.Affine.real line 22
  5. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_cst line 25
  6. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_coord line 27
  7. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_zero line 29
  8. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_add line 31
  9. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_sub line 34
  10. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_smul line 37
  11. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.real_sum line 40
  12. lemma OAI.AlgorithmicThinTrees.RationalForms.Affine.ext_real line 47
  13. def OAI.AlgorithmicThinTrees.RationalForms.pencil line 61
  14. lemma OAI.AlgorithmicThinTrees.RationalForms.pencil_realEval line 68
  15. lemma OAI.AlgorithmicThinTrees.RationalForms.symmetric_of_real line 80
  16. lemma OAI.AlgorithmicThinTrees.RationalForms.blockDiagonal_psd line 84
  17. lemma OAI.AlgorithmicThinTrees.RationalForms.blockDiagonal_map line 108
  18. lemma OAI.AlgorithmicThinTrees.RationalForms.diagonal_map line 115
  19. lemma OAI.AlgorithmicThinTrees.RationalForms.fromBlocks_map line 122
  20. lemma OAI.AlgorithmicThinTrees.RationalForms.fromBlocks_psd line 129
  21. lemma OAI.AlgorithmicThinTrees.RationalForms.submatrix_equiv_psd line 145