OAI/Combinatorics/Chromatic/GradedAlgebra/ClearedSeparation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_rat_smul line 10
2. lemma OAI.ElementaryPositivity.LaurentAtInfinity.rat_smul_mul line 13
3. lemma OAI.ElementaryPositivity.RawShuffle.normalize_cleared_tensor line 27
4. lemma OAI.ElementaryPositivity.RawShuffle.separation_of_cleared line 39
5. lemma OAI.ElementaryPositivity.RawShuffle.separation_shuffle_grid line 48