how to find where the instance are define ?

Stream: maths

[orlando]

Hello,

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 has_mul on 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]

#check (by apply_instance : has_mul (linear_map _ _))

[orlando]

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:

OK !!

[Reid Barton]

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]

An other little question what is the difference between rw and erw ? I thinck erw is more powerful but i don't understand really the difference ?

[Keeley Hoek]

I don't even know what the e stands for. expensive?

[Bhavik Mehta]

extended, I think

[Yury G. Kudryashov]

erw unfolds more definitions while trying to match LHS with the goal

[orlando]

Ok Yury ! It make sense !