OAI/Combinatorics/Progressions/Polynomial/DiagonalTensorPolynomial.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.tensorDiagonalPolynomialline 12 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_evalline 16 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_addline 21 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_mulline 27 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_mapline 32 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_eq_sum_monomialline 37 - theorem
OAI.Erdos3.tensorDiagonalPolynomial_multilinear_evalline 42