How to search a theorem

Stream: new members

[Xipan Xiao]

I know that if f: A → B between commutative rings satisfies the following conditions:

1. All element of a submonoid S of A are sent to units;
2. ker f is exactly the zero divisors of elements of S;
3. All elements of B can be written as f(x)/f(s) for some x in A and s in S.
   then f is just the localization A → S^{-1}A. I looked through the Localization and IsLocalization namespaces quickly but didn't find a match yet. Is there a trick, or some general guidance, for such kind of theorem searches? Or even is there a theorem searcher so that I can input my hypothesis types, and it returns the matches? I guess that exact? is the thing I needed, but are there anything else?

[Matt Diamond]

is there a theorem searcher

• https://leansearch.net/
• https://loogle.lean-lang.org/
• https://www.moogle.ai/

[Matt Diamond]

Loogle sounds the closest to what you're asking for, in terms of searching by types

... though honestly I don't have much experience with the others, so maybe they do the same thing

[Kevin Buzzard]

What you write is the definition of docs#IsLocalization and the API for that is all you need. If you want more precise help then you should ask a more precise question with a #mwe . In particular your use of the phrase "f is just..." needs clarification formally.

[Justin Asher]

Matt Diamond said:

is there a theorem searcher

• https://leansearch.net/
• https://loogle.lean-lang.org/
• https://www.moogle.ai/

I also recently setup www.leanexplore.com. Would be happy for any feedback! Am still working on optimizing the search algorithm.

[Kevin Buzzard]

(brief feedback -- I used it once so far and it worked great!)

[Justin Asher]

Here is your query, for reference, @Xipan Xiao. It seems to point you to an instance of the desired class that Kevin mentioned.

[Bolton Bailey]

For the reference of others, there is also a draft blog post at blog#75 containing a write up of various search engines. (Apparently this was reviewed months ago, but I didn't notice or address the comments until now, sorry about that)