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
• Frobenius normal form (using the above point), Jordan normal form

Bilinear algebra

• diagonalization of normal endomorphisms This is coming, self-adjoint maps are done in #9995

Group theory

• orthogonality of irreducible characters

Complex analysis

• Cauchy formula Yury is working on it
• Analyticity of holomorphic functions
• residue theorem
• zeros and poles of a meromorphic function are isolated

Integration and Fourier theory

• change of variables formula in higher dimensions
• Dirichlet theorem and Fejer theorem for Fourier series
• Fourier inversion theorem, Plancherel’s theorem

Probability theory

• Weak and strong law of large numbers
• Central limit theorem