mathlib3

def4814c - refactor(topology/algebra/module): continuous semilinear maps (#9539)

refactor(topology/algebra/module): continuous semilinear maps (#9539) Generalize the theory of continuous linear maps to the semilinear setting. We introduce a notation `∘L` for composition of continuous linear (i.e., not semilinear) maps, used sporadically to help with unification. See #8857 for a discussion of a related problem and fix. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>