flâneur

Undergrad math not in mathlib

leanprover-community.github.io · 1,025 words · saved by 1 readers

This gives pointers to undergraduate maths topics that are currently missing in mathlib. The list is gathered from the French curriculum. There is also a page listing undergraduate maths topics that are already in mathlib. If you want to work on an item from this list then you should first check the pull requests list to see whether it is already coming, then the issues list to see whether it is discussed there, and finally talk about this idea on Zulip. To update this list, please submit a PR modifying docs/undergrad.yaml in the mathlib repository. Duality: orthogonality. Finite-dimensional vector spaces: rank of a system of linear equations. Multilinearity: special linear group. Matrices: elementary row operations, elementary column operations, Gaussian elimination, row-reduced matrices. Structure theory of endomorphisms: diagonalization, triangularization, invariant subspaces of an endomorphism, kernels lemma, Jordan normal form. Linear representations: irreducible representation, e

Undergrad math not in mathlib Missing undergraduate mathematics in mathlib This gives pointers to undergraduate maths topics that are currently missing in mathlib. The list is gathered from the French curriculum . There is also a page listing undergraduate maths topics that are already in mathlib . If you want to work on an item from this list then you should first check the pull requests list to see whether it is already coming, then the issues list to see whether it is discussed there, and finally talk about this idea on Zulip . To update this list, please submit a PR modifying docs/undergra

related reading