OAI/Combinatorics/Progressions/Polynomial/MixedBoxPolynomial.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors_orbit_monoline 18 - def
OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxPolynomialline 26 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxPolynomial_monoline 33 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxPolynomial_eq_testline 48 - theorem
OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest_symbolline 53