Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 17:31 bafe207d

View on Github →

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.

Estimated changes