Commit 2021-09-07 03:49 f157b6df

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.