Big missing undergraduate theorems

The purpose of this page is to list items from the Missing undergraduate mathematics in mathlib that milestone results. The structure of this file follows the undergrad list structure.

There is also another page listing trivial targets, and a page for low hanging fruits.

Linear algebra

• Classification of finite type modules over principal ideal domains, including the case of finite abelian groups. We have existence, not yet uniqueness.
• Frobenius normal form (using the above point), Jordan normal form

Bilinear algebra

• diagonalization of normal endomorphisms Done in the semilinear paper, needs to be PR'd.

Group theory

• orthogonality of irreducible characters see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Subrepresentations for the state of representation theory

Complex analysis

• residue theorem
• zeros and poles of a meromorphic function are isolated. There is some work on this.

Integration and Fourier theory

• The change of variables formula in higher dimensions is done, but we need specialization to polar and spherical coordinates
• Dirichlet theorem and Fejer theorem for Fourier series
• Fourier inversion theorem, Plancherel’s theorem

Probability theory

• Central limit theorem