Zulip Chat Archive

Stream: maths

Topic: submodule map


view this post on Zulip 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 ?

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 09:15):

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

view this post on Zulip Mario Carneiro (Apr 26 2020 at 09:22):

I think it would be okay to make it explicit

view this post on Zulip 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 '

view this post on Zulip 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

view this post on Zulip 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