Documentation

Mathlib.RingTheory.Polynomial.Hermite.Basic

Hermite polynomials #

This file defines Polynomial.hermite n, the nth probabilists' Hermite polynomial.

Main definitions #

Results #

References #

noncomputable def Polynomial.hermite :

the probabilists' Hermite polynomials.

Equations
Instances For
    @[simp]

    The recursion hermite (n+1) = (x - d/dx) (hermite n)

    Lemmas about Polynomial.coeff #

    theorem Polynomial.coeff_hermite_of_lt {n k : } (hnk : n < k) :
    @[simp]
    @[irreducible]

    Because of coeff_hermite_of_odd_add, every nonzero coefficient is described as follows.