  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
\textsf{mathlib} 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.
