Commit 2020-08-16 06:05 765e4605
View on Github →feat(ring_theory/polynomial/homogeneous): definition and basic props (#3223) This PR also move ring_theory/polynomial.lean to ring_theory/polynomial/basic.lean This PR is part of bringing symmetric polynomials to mathlib, and besided that, I also expect to add binomial polynomials and Chebyshev polynomials in the future. Altogether, this motivates the starting of a ring_theory/polynomial directory. The file basic.lean may need cleaning or splitting at some point.