mathlib

b17e2720 - feat(ring_theory/polynomial): add properties of `coeff (hermite n)` (#18837)

feat(ring_theory/polynomial): add properties of `coeff (hermite n)` (#18837) Added lemmas showing recursive relations between coefficients of `polynomial.hermite n`: - `coeff (hermite (n + 1)) 0 = -(coeff (hermite n) 1)` - `coeff (hermite (n + 1)) (k + 1) = coeff (hermite n) k - (k + 2) * (coeff (hermite n) (k + 2))` Showed some more properties of the coefficients of Hermite polynomials: - for `k>n`, the `k`th coefficient of the `n`th Hermite polynomial is zero - the `n`th Hermite polynomial is of degree `n` - the Hermite polynomials are monic Co-authored-by: Jake Levinson [levinson.jake@gmail.com](mailto:levinson.jake@gmail.com) Co-authored-by: lukemantle <62187700+lukemantle@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>