Commit 2021-09-07 03:49 f157b6dfView on Github →
feat(linear_algebra): introduce notation for
This PR introduces new notation for the composition of linear maps and linear equivalences:
linear_equiv.trans. This will be needed by an upcoming PR generalizing linear maps to semilinear maps (see discussion here): in some places, we need to help the elaborator a bit by telling it that we are composing plain linear maps/equivs as opposed to semilinear ones. We have not made the change systematically throughout the library, only in places where it is needed in our semilinear maps branch.