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

modified def alg_hom.to_linear_map
modified def algebra.lmul_left
modified def algebra.lmul_right
modified def is_linear_map.mk'
modified def dual_tensor_hom
modified theorem rank_comp_le2
modified def finsupp.restrict_dom
modified def linear_map.compl₂
modified def linear_map.compr₂
modified theorem linear_map.lcomp_apply
modified def linear_map.llcomp
modified def linear_map.lsmul
modified def tensor_product.curry
modified def tensor_product.lift
modified def tensor_product.map
modified def tensor_product.mk