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.

Estimated changes

modified theorem continuous_linear_equiv.ext
modified theorem continuous_linear_map.ext