mathlib3

c6275ef4 - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials (#18739)

feat(ring_theory/polynomial): define the probabilist's Hermite polynomials (#18739) Define the Hermite polynomials recursively, and show this is equivalent to the result of iterating the operation `x - d/dx` on the constant polynomial `1`. Future PRs will include several equivalent characterizations: - Recursive and explicit expressions for the coefficients - Definition based on the nth derivative of the Gaussian function Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: lukemantle <62187700+lukemantle@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>