mathlib

066ecdb4 - feat(ring_theory/polynomial): show gaussian form of `hermite n` (#18896)

feat(ring_theory/polynomial): show gaussian form of `hermite n` (#18896) Show the equivalence of the polynomial form of the Hermite polynomials to the explicit form involving derivatives of the gaussian function. Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: lukemantle <lukeomantle@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>