mathlib

d27ddb49 - chore(linear_algebra/basic): rewrite `p.comap q.subtype` to `comap q.subtype p` (#3725)

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`.