mathlib

fa3b6222 - refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551)

refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551) Generalize the theory of linear isometries to the semilinear setting. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>