## Stream: maths

### Topic: how to find where the instance are define ?

#### orlando (Apr 22 2020 at 15:29):

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 (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:

OK !!

#### 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  rw  and 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. expensive?

#### 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