## Stream: maths

### Topic: submodule map

#### orlando (Apr 26 2020 at 08:11):

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 (Apr 26 2020 at 09:15):

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

#### Mario Carneiro (Apr 26 2020 at 09:22):

I think it would be okay to make it explicit

#### orlando (Apr 26 2020 at 09:30):

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 (Apr 26 2020 at 09:32):

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 (Apr 26 2020 at 16:22):

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

Last updated: May 14 2021 at 19:21 UTC