Commit 2020-08-08 13:01 d27ddb49

chore(linear_algebra/basic): rewrite p.comap q.subtype to comap q.subtype p (#3725) @PatrickMassot requested this change in the review of #3720:

I find this statement very difficult to read. I think this is a bad use of dot notation, it really feels like p is pulling back q.subtype instead of the other way around (and even the docstring is suggesting that!). The same problem happens with filter.(co)map and always try to avoid it. I would open submodule and then write comap q.subtype p ≃ₗ[R] p.