OAI/Combinatorics/ThinTrees/Expectation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StrongThinTree.MSS.detLinearline 14 - lemma
OAI.StrongThinTree.MSS.detLinear_applyline 17 - lemma
OAI.StrongThinTree.MSS.detLinear_mapline 21 - lemma
OAI.StrongThinTree.MSS.det_piecewise_mulline 31 - lemma
OAI.StrongThinTree.MSS.det_add_rankOneline 44 - lemma
OAI.StrongThinTree.MSS.det_linear_pencil_coeff_oneline 64