linear map/equiv notation

Stream: general

[Adam Topaz]

Is the following mismatch intended?

notation M ` ≃ₗ[`:50 R `] ` M₂ := ...
notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := ...

I ran into some issues with the equiv notation in the following example:

example {A : Type*} [ring A] :
  (A × A ≃ₗ[A] A × A) =
  ((A × A) ≃ₗ[A] (A × A)) := rfl -- fails

example {A : Type*} [ring A] :
  (A × A ≃ₗ[A] A × A) → A := prod.fst -- typechecks