Undergrad low hanging fruits

The purpose of this page is to list items from the Missing undergraduate mathematics in mathlib that are expected to be rather easy to get. The structure of this file follows the undergrad list structure.

There is also another page listing trivial targets, and a page for big missing theorems.

Linear algebra

Matrices

• elementary row operations
• elementary column operations
• Gaussian elimination
• row-reduced matrices

Linear representations

• irreducible representation
• Schur's lemma
• examples: this is a bit vague, but it would be nice to have a couple of classical elementary examples of representation of finite groups. At least permutation representations and cyclic groups acting by rotations on a plane.

Polynomial rings

• relationship between the coefficients and the roots of a split polynomial see #14908, #15008
• Newton's identities see https://leanprover-community.github.io/mathlib_docs/ring_theory/polynomial/symmetric.html

Field Theory

• ℝ(X)-partial fraction decomposition
• ℂ(X)-partial fraction decomposition

Bilinear and Quadratic Forms Over a Vector Space

Orthogonality

Note that we already have declaration whose docstring-pretend to be Sylvester's law of inertia, in linear_algebra.quadratic_form.real but they do not prove that the number of 1 and -1 is independent of the basis.

• Sylvester's law of inertia
• real classification
• complex classification

Endomorphisms

• simultaneous diagonalization of two real quadratic forms, with one positive-definite
• polar decompositions in GL(n, ℝ)
• polar decompositions in GL(n, ℂ)

Low dimensions

• classification of elements of O(3, ℝ)

Single Variable Real Analysis

Numerical series

We've been postponing this for a long time because we have things about (unordered) infinite sums in topological groups, but also because we couldn't decide whether series are necessarily index by ℕ or could use more general indexing sets. Given that we only care about series for undergrad coverage, I think we should go with ℕ. Add a definition convergent_series (u : ℕ → E) : Prop where E is a real normed space, and prove everything in this context.

• Convergence of real valued-series
• summation of comparison relations
• comparison of a series and an integral
• error estimation
• absolute convergence
• products of series
• alternating series

Integration

• integral over a segment of piecewise continuous functions: we should probably state and prove that such function are (Lebesgue) integrable and their integral can be computed using Riemann sums.
• antiderivatives
• Riemann sums
• improper integrals
• absolute vs conditional convergence of improper integrals
• comparison test for improper integrals

Convexity

• continuity and differentiability of convex functions