OAI/Combinatorics/Chromatic/Shuffle/TargetEmbedding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RawShuffle.targetEmbedding line 13
2. lemma OAI.ElementaryPositivity.RawShuffle.gridEmbedding_square line 39
3. lemma OAI.ElementaryPositivity.RawShuffle.gridPolynomial_four_realization line 48
4. lemma OAI.ElementaryPositivity.RawShuffle.targetEmbedding_algebraMap line 61
5. lemma OAI.ElementaryPositivity.RawShuffle.targetEmbedding_left_kernel line 69
6. lemma OAI.ElementaryPositivity.RawShuffle.targetEmbedding_right_kernel line 93
7. lemma OAI.ElementaryPositivity.RawShuffle.grid_shape_transfer line 117
8. def OAI.ElementaryPositivity.RawShuffle.castTensor line 156
9. lemma OAI.ElementaryPositivity.RawShuffle.quotientTensor_cast_zero line 162
10. def OAI.ElementaryPositivity.RawShuffle.targetValueAt line 170
11. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_apply line 179
12. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_injective line 185
13. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_tmul line 192
14. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_independent line 202
15. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_cast line 212
16. lemma OAI.ElementaryPositivity.RawShuffle.targetValueAt_mul line 222