Overview
Mathlib4 is the community-driven mathematical library for the Lean4 theorem prover, with over a million lines of formalized mathematics spanning algebra, analysis, topology, number theory, and the tactics that automate reasoning over them. Contributing to Mathlib4 means writing and proving definitions, lemmas, and tactics that the broader Lean community then builds on — a small chance to participate directly in the ongoing formalization of modern mathematics.
Below are the pull requests I have submitted or plan to submit, with links to the diffs and a short note on what each one changes or proves.
Pull Requests
- #37933 (Merged) — feat(LinearAlgebra/Matrix/Hermitian): A block-diagonal matrix is Hermitian iff each block is Hermitian. Add two lemmas characterizing when a block diagonal matrix is Hermitian:
blockDiagonal' Mis Hermitian if and only if each blockM iis Hermitian, andblockDiagonal M(block diagonal matrix whose components are all equal) is Hermitian if and only if each blockM iis Hermitian. - More coming soon!