Finding axioms and theorems in mathlib

Stream: new members

[Victor Miller]

I'm in my fourth iteration of trying to get into Lean. I did go through the Natural Numbers Game, which was fun a challenging, though the meaning and scope of many tactics was still not clear. Right now, in trying to do the exercises from Theorem proving in Lean it seems necessary to find the axioms and theorems pertaining to a particular structure (such as Group). Is there some organized way of doing this, besides trying to guess what they might be called?

[Patrick Massot]

it seems necessary

No it isn't.

[Patrick Massot]

If you tell us about a more specific problem you have then you will get an even more useful answer.

[Alex J. Best]

In general though, the tactics apply?, rw? and exact? are good ways of finding lemmas that apply in a given goal state in some way. I would imagine that TPIL is set up so that the exercises can be done with only the lemmas introduced earlier in the same text though

[Matt Diamond]

It's also useful to just read through the docs for the particular subject you're working in... you start to pick up on naming patterns and it makes it easier to guess when searching for them.

[Victor Miller]

So how do I find things in Mathlib? RIght now I wanted to state (and prove) a theorem about finite dimensional vector spaces over R, along with various norms. I've been looking over the mathlib4-docs for about an hour and haven't been able to find what I want. As a mathematician, I can just say: Let $v$ be a finite dimensional vector space over $\mathbb{R}$ and everybody knows what that is. Is there an easy way to search for such things?

[Alex J. Best]

Moogle is one such tool, e.g. https://www.moogle.ai/search/raw?q=finite%20dimensional%20vector%20space and the 4th result is the one you want

[Victor Miller]

Alex J. Best said:

Moogle is one such tool, e.g. https://www.moogle.ai/search/raw?q=finite%20dimensional%20vector%20space and the 4th result is the one you want

Alex, Thanks.

[Luigi Massacci]

You may also be interested in chapter 10 of #mil (as well as the other 10 probably) for some explanations concerning vector spaces and so on in Lean