orlando (Apr 22 2020 at 15:29):
I don't understand how to find where the instance are define :
In this example, i have acces to
* -notation so i have an instance of
M→ₗ[R]M but where is it define ? Is there exist some tatict to find information in the code of mathlib ? thx
import linear_algebra.basic import algebra.module variables (M : Type )(R :Type) [ring R] [add_comm_group M] [add_comm_group M] [module R M] variables (f g : M→ₗ[R]M) example : f * g = linear_map.id := sorry
Kenny Lau (Apr 22 2020 at 15:30):
#check (by apply_instance : has_mul (linear_map _ _))
orlando (Apr 22 2020 at 15:41):
Thx Kenny, you give me an idea ! just write
linear_map.has_mul and click to go in the file where is define
I'm stupid some time :sweat_smile:
Reid Barton (Apr 22 2020 at 15:42):
It's not at all guaranteed that you will be able to guess the name of the instance in this way, but yes it will often work.
orlando (Apr 22 2020 at 16:20):
An other little question what is the difference between
erw ? I thinck
erw is more powerful but i don't understand really the difference ?
Keeley Hoek (Apr 22 2020 at 17:03):
I don't even know what the
e stands for.
Bhavik Mehta (Apr 22 2020 at 17:10):
extended, I think
Yury G. Kudryashov (Apr 22 2020 at 17:15):
erw unfolds more definitions while trying to match LHS with the goal
orlando (Apr 22 2020 at 17:16):
Ok Yury ! It make sense !
Last updated: May 14 2021 at 18:28 UTC