mathlib

bafe207d - chore(linear_algebra): remove `→ₗ` notation where the ring is not specified (#8778)

chore(linear_algebra): remove `→ₗ` notation where the ring is not specified (#8778) This PR removes the notation `M →ₗ N` for linear maps, where the ring is not specified. This is not used much in the library, and is needed for an upcoming refactor that will generalize linear maps to semilinear maps. See the discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Semilinear.20maps).