Commit 2021-09-07 03:49 f157b6df
View on Github →feat(linear_algebra): introduce notation for linear_map.comp
and linear_equiv.trans
(#8857)
This PR introduces new notation for the composition of linear maps and linear equivalences: ∘ₗ
denotes linear_map.comp
and ≫ₗ
denotes 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.