OAI/Combinatorics/ThinTrees/Matrix.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StrongThinTree.quadratic_cauchy_schwarzline 14 - lemma
OAI.StrongThinTree.rankOne_quadraticline 25 - lemma
OAI.StrongThinTree.posDef_solveline 30 - theorem
OAI.StrongThinTree.resistance_orderline 35 - theorem
OAI.StrongThinTree.resistance_antitoneline 66