Undergrad TODO trivial targets

The purpose of this page is to list items from the Missing undergraduate mathematics in mathlib that are expected to be very easy to get. Some of them are definitely there, but missing from the data file so it's only a matter of taking time to figure out the best declaration to use. Some may or may not be there. Others are presumably obtainable within at most one hour of work. The structure of this file follows the undergrad list structure.

There is also another page listing low hanging (but not trivial) fruits, and a page for big missing theorems.

Linear algebra

Duality

• orthogonality This should be a definition together with at least basic lemmas about the orthogonal of the bottom and top subspaces, of an intersection, union, sum.

Finite-dimensional vector spaces

• rank of a system of linear equations

Multilinearity

• special linear group We have the matrix version but need the endomorphism versions

Structure theory of endomorphisms

The first three items below are only definitions. We should have a look at how the spectral theorem is currently stated.

• diagonalization
• triangularization
• invariant subspaces of an endomorphism
• kernels lemma

Exponential

We need to hook things in analysis.special_functions.exponential to finite dimensions and matrices

• endomorphism exponential

Classical automorphism groups

We need both the matrix and endomorphism versions of these eventually, but note that only the matrix version is currently a "trivial target", the endomorphism version needs to wait for WIP on defining the adjoint.

• special orthogonal group
• special unitary group

Algebra

• algebra over a commutative ring This was discussed a lot already: see e.g. this PR

Bilinear and Quadratic Forms Over a Vector Space

Bilinear forms

• rank of a bilinear form

Low dimensions

• classification of elements of O(2, ℝ)

Affine and Euclidean Geometry

General definitions

• equations of affine subspace: It would be nice to know that the preimage (#10795) of a point under an affine map is an affine subspace and that any subspace is such a preimage. In a truly undergrad spirit we should also have explicit special cases for lines and planes in ℝ² and ℝ³.
• group generated by homotheties and translations
• transformations fixing a basis of directions

Single Variable Real Analysis

Taylor-like theorems

• Taylor's theorem with little-o remainder
• Taylor's theorem with integral form for remainder
• Taylor series expansions

Integration

• change of variable: we already have it, need to find the declaration (note this is in the single variable section)

Sequences and series of functions

• normal convergence it would be nice to include continuuity and differentiability of the limit
• differentiability of the limit

Topology

Normed vector spaces on $\mathbb{R}$ and $\mathbb{C}$

• equivalent norms: the content is already there, but we may need to add a recognizable declaration

Multivariable calculus

Differential calculus

• directional derivative
• partial derivatives
• Jacobian matrix
• gradient vector
• Hessian matrix
• $k$-th order partial derivatives

Differential equations

• maximal solutions: I guess this is already somewhere?

Measures and integral Calculus

Integration

• differentiability of integrals with respect to parameters: we already have that, we need to find the relevant declaration