Formalized functional analysis with semilinear maps

Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth

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 part…