mathlib

f157b6df - feat(linear_algebra): introduce notation for `linear_map.comp` and `linear_equiv.trans` (#8857)

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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Semilinear.20maps)): 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.