How do I search within Mathlib 4? #dumb question

Stream: mathlib4

[Mark Santa Clara Munro]

For example, I feel like there must be something in the library I can apply for the following:

import Mathlib

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m] [SMul R α] [Add α] [Zero α] [Mul α]

lemma scalarscalarmatrix [Field α] [Field R] (M : Matrix m n α) (x : R) (y : R) (hx : x ≠ 0) (hy : y ≠ 0)
  : x • (y • M) = (x • y) • M := by
  ext i j
  simp

I feel like there has to be something that I can use for this, but I really don't know how to search the library to try to find things I feel like have to have been done.

[Kim Morrison]

You've done it again: [Mul α] and [Field α] mean you have two completely unrelated multiplications on α.

[Mark Santa Clara Munro]

I'm confused, does that do a multiplication on alpha? I thought it would allow for other properties. Also, could you answer my question if possible?

[Bolton Bailey]

Yes, Kim is saying that [Field α] gives you multiplication on α, and that having [Mul α] (and [Add α] [Zero α]) is redundant and likely to give you bugs.

docs#smul_assoc is probably what you're looking for for the lemma. (I can't check because the web editor is not starting for me for some reason).

[Johan Commelin]

You can search for that result using by exact? but only once the statement is correct. Hence Kim's remark is actually very much on topic. As stated you are searching for a result that is quite possibly not true.

[Kim Morrison]

The fact that the hypotheses so far include SMul R \a but nothing that states any axioms about this scalar multiplication means that the lemma as stated is surely false.

[Mark Santa Clara Munro]

Could you explain what it means for it to be surely false? Is it mathematically incorrect or do you mean I have to include other things so that I am able to prove it? What should I include that would state any axioms about this scalar multiplication? I'm sorry if these are very trivial questions, I am trying to learn

[Bolton Bailey]

It is mathematically incorrect, and to make it mathematically correct/to be able to prove it, you would have to add other things.

Here is what the proof should look like with the lemma I suggested, but you can see it complains about not being able to synthesize IsScalarTower.

import Mathlib

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m] [SMul R α]

lemma scalarscalarmatrix [Field α] [Field R] (M : Matrix m n α) (x : R) (y : R) (hx : x ≠ 0) (hy : y ≠ 0)
  : x • (y • M) = (x • y) • M := by
  rw [smul_assoc] -- failed to synthesize IsScalarTower R R (Matrix m n α)

What is going on is that there is a definition of multiplication on α, and there is a definition of multiplication on R, and there is a definition of scalar multiplication of α on R. But there is nothing to say that this scalar multiplication that is defined makes any normal sense. It could be the case that α and R are the rationals, but the scalar multiplication is not normal multiplication but some weird function that returns -17 when the denominator of the left hand side is a prime and 37 otherwise.

So what is needed is a new hypothesis that says that this scalar multiplication respects the usual associative law. In other words, what is needed is [IsScalarTower R R α]. And this makes the lemma work:

import Mathlib

variable {m n : Type*} {α R : Type*}
variable [DecidableEq m] [SMul R α]

lemma scalarscalarmatrix [Field α] [Field R] [IsScalarTower R R α] (M : Matrix m n α) (x : R) (y : R) (hx : x ≠ 0) (hy : y ≠ 0)
  : x • (y • M) = (x • y) • M := by
  rw [smul_assoc] -- works

[Kevin Buzzard]

Furthermore you can delete hx and hy, they're unused.

[Kevin Buzzard]

Things like [SMul R α] don't mean "magic up some natural action of R on alpha", they mean literally nothing more than "magic up a completely arbitrary function which eats elements of r of R and a of alpha, and returns an element of alpha with notation r • a -- this is just the assumption that the notation makes syntactic sense, not that it has any mathematical meaning. [SMul R α] is just adding notation. Whereas the assumption [IsScalarTower R R α] is adding an axiom, namely that r • (s • a) = (r * s) • a, which is what you need to complete your proof.

[Kevin Buzzard]

If you're a beginner then you might be better off working with exercises which other people have written for now, because writing correct theorem statements is much harder than writing easy proofs if you're just learning.

[Mark Santa Clara Munro]

Thank you so much for the help and the thorough explanation! That is very helpful

[Mark Santa Clara Munro]

I honestly agree with that of being better off working with exercises which other people have written for now, but I am doing summer research with a professor and these are the things we are working on and that I am told to work on. I will try and add on exercises that other people have written as well, but I will probably still have to ask questions here on zulip and trying to go through documentation to figure out what to write

[Anthony Bordg]

How can I search the library efficiently to find the theorem ∀ (P : Prop), P → P?

[Matthew Ballard]

#loogle is probably your best bet. Maybe #moogle

[Matthew Ballard]

Hmm. No linkfiers.

[Matthew Ballard]

@loogle (P : Prop), P -> P

[Matthew Ballard]

and moogle.ai

[Matthew Ballard]

NB: I am not a loogle syntax expert (I occasionally use it to look for constants)

[Matthew Ballard]

Or you can use

example : ∀ (P : Prop), P → P := by exact?

[Kevin Buzzard]

(by exact?)

[Anthony Bordg]

Thank you Matthew for the references to Loogle and Moogle which I was not aware of (unfortunately, they didn't prove effective on this particular instance), but exact?# did work.