finding instance declaration

Stream: Is there code for X?

[Justin Thomas]

In linear_algebra/basic.lean there is a lemma I am trying to use

lemma span_smul_eq_of_is_unit (s : set M) (r : R) (hr : is_unit r) :
  span R (r • s) = span R s

When I try to use this in my context, ( R = 𝕜, r = c, s = {g}, M = 𝕜[X] )

lemma should_be_simple (g : 𝕜[X]) (c : 𝕜) : span 𝕜[X] (c • ({g}: set 𝕜[X])) = span 𝕜[X] ({g} : set 𝕜[X]) := sorry

lean complains:

failed to synthesize type class instance for
𝕜 : Type u_1,
_inst_1 : field 𝕜,
g : 𝕜[X],
c : 𝕜
⊢ has_scalar 𝕜 (set 𝕜[X])

I am trying to see if I'm just reading the syntax wrong, so I want to chase down the has_scalar instance that is being used in the lemma above. I did some text searches like 'instance : has_scalar...' but I feel like there has to be a better way. I am looking more for strategies to get me past questions like this more than just an answer to this particular instance.

[Heather Macbeth]

If you go to the docs, docs#has_scalar, you'll see a list of all of the instances. This is a good place to start.

[Heather Macbeth]

Here I see docs#polynomial.has_scalar on that list.

[Johan Commelin]

@Justin Thomas Did you intend to write (c • ({g}: set 𝕜[X]))? Or do you mean ({c • g}: set 𝕜[X])?

[Yaël Dillies]

They are the same thanks to docs#set.smul_singleton

[Heather Macbeth]

That list doesn't contain "transitive" instances (e.g. a normed space is a module is a distrib_mul_action is a mul_action is a has_scalar), so there's still some guesswork.

[Justin Thomas]

@Heather Macbeth thanks. I did not know about that. Is it auto-generated? So guaranteed to be up to date? seems like lean should combine set.has_scalar and polynomial.has_scalar. I don't know how to give it a hint to find these.

[Heather Macbeth]

Yes, it's autogenerated every two hours.

[Heather Macbeth]

In this case you might need to say open_locale pointwise to get the docs#set.has_scalar_set instance.

[Heather Macbeth]

See the docstring on that instance.

[Justin Thomas]

@Johan Commelin I mean (c • ({g}: set 𝕜[X]))because I am trying to match (r • s)in span_smul_eq_of_is_unit.

[Johan Commelin]

Fair enough. So yeah, then you probably need to have open_locale pointwise as Heather points out.

[Justin Thomas]

Heather Macbeth thanks so much! open_locale pointwise is what I was missing!! (off to figure out what that means...)

[Justin Thomas]

bonus question. Why do I need to put the {g}: set 𝕜[X] extra type annotation?
Here is what I had at one point that lean really dislikes

-- maybe is_unit c ?
lemma should_be_simple (g : 𝕜[X]) (c : 𝕜) : span 𝕜[X] c • {g} = span 𝕜[X] {g} := sorry

[Heather Macbeth]

Here {g} is just a notation, docs#has_singleton, and Lean has to figure out what kind of singleton is meant (set? finset? ...)

[Heather Macbeth]

I actually introduced a notation before because of precisely this issue

[Heather Macbeth]

https://github.com/leanprover-community/mathlib/blob/48eacc63751375da61238b90773c4208e768eabc/src/linear_algebra/span.lean#L307

[Heather Macbeth]

So you can write 𝕜[X] ∙ g for span 𝕜[X] {g} (and it builds in that it's the set-singleton that's meant.)

[Justin Thomas]

Heather Macbeth said:

So you can write 𝕜[X] ∙ g for span 𝕜[X] {g} (and it builds in that it's the set-singleton that's meant.)

much nicer. Is there a way to discover notations in the docs similar to instances?

[Heather Macbeth]

No, in fact; it would be nice but there's currently no autogeneration of documentation for notation.