Zulip Chat Archive

Stream: maths

Topic: how to find where the instance are define ?


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

view this post on Zulip Kenny Lau (Apr 22 2020 at 15:30):

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

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

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

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

view this post on Zulip Keeley Hoek (Apr 22 2020 at 17:03):

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

view this post on Zulip Bhavik Mehta (Apr 22 2020 at 17:10):

extended, I think

view this post on Zulip Yury G. Kudryashov (Apr 22 2020 at 17:15):

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

view this post on Zulip orlando (Apr 22 2020 at 17:16):

Ok Yury ! It make sense !


Last updated: May 14 2021 at 18:28 UTC