OAI/Probability/SpanningForest/OrderedMinorCounting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.OrderedMinorCounting.embeddingRange line 14
2. lemma OAI.Problem336.OrderedMinorCounting.mem_embeddingRange line 17
3. lemma OAI.Problem336.OrderedMinorCounting.card_embeddingRange line 22
4. def OAI.Problem336.OrderedMinorCounting.embeddingFiberEquiv line 26
5. lemma OAI.Problem336.OrderedMinorCounting.card_embedding_fiber line 55
6. theorem OAI.Problem336.OrderedMinorCounting.sum_embeddingRange line 66
7. def OAI.Problem336.OrderedMinorCounting.minorSquare line 81
8. lemma OAI.Problem336.OrderedMinorCounting.minorSquare_embeddingRange line 85
9. lemma OAI.Problem336.OrderedMinorCounting.sum_embedding_eq_sum_injective line 98
10. theorem OAI.Problem336.OrderedMinorCounting.weighted_gram_det_unordered line 107