Commit 2021-10-05 08:58 def4814c
View on Github →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.