# Formalized functional analysis with semilinear maps

arXiv: https://arxiv.org/abs/2202.05360 · HTML: https://mlsanity.com/paper/2202.05360/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Feb 2022.

## Built on by (most cited first, 2 of 2)

- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)

## Abstract (arXiv)

Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean's textsfmathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fr'echet--Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonn'e and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.