submodule map

Stream: maths

[orlando]

Hello,
it's normal that in the file linear_algebra.basic ligne 509. The function

lemma map_mono {f : M →ₗ[R] M₂} {p p' : submodule R M} : p ≤ p' → map f p ≤ map f p' :=
image_subset _

have f for implicit variables ! If i understand it's not a good idea ?

[Kevin Buzzard]

That does look surprising to me. Sometimes there is no "best way" for the brackets though

[Mario Carneiro]

I think it would be okay to make it explicit

[orlando]

If i understand the problem is if some one have use this function in mathlib this cause big trouble ? I don't understand exactly :grinning_face_with_smiling_eyes: i just make the explicit one with a '

[Kevin Buzzard]

You could change it in mathlib and then recompile all of mathlib with lean --make and see what breaks. You might be able to make mathlib better this way

[Yury G. Kudryashov]

Or push your branch to github and let CI recompile mathlib for you. I often do this because my laptop is not very fast.