How to find `nat` theorms in mathlib?

Stream: new members

[Martin C. Martin]

How do I find theorems related to addition, multiplication, etc on the natural numbers? Grepping through the source of mathlibisn't giving me any love, e.g. neg_add_self seems to only be defined as a lemma in ./category_theory/abelian/non_preadditive.lean . I currently need n + m.succ = n.succ + m but I'm sure there will be many, many more I need in the future.

[David Renshaw]

Have you tried the library_search tactic?

[Huỳnh Trần Khanh]

I'm pretty sure as mathlib is written in a general style, you won't find many theorems proven specifically for natural numbers. There are theorems that apply for natural numbers but they are actually proven for something more generic. This stuff is too high for me though, but I'm pretty sure this is the case. library_search should always work.

[Ruben Van de Velde]

Guessing names and vscode autocompletion - in this case, I assumed it would have add_succ or succ_add in the name, and probably be in the nat namespace. Turns out it's neither of those (they say both sides of your equation are equal to (n + m).succ, but it is nat.succ_add_eq_succ_add

[Ruben Van de Velde]

One issue with grep is that many theorems about additive groups (etc) are written only in multiplicative form, and to_additive translates them automatically

[Ruben Van de Velde]

For example:

@[to_additive] lemma inv_mul_self (a : G) : a⁻¹ * a = 1 := mul_left_inv a

which defines neg_add_self

[Huỳnh Trần Khanh]

But the generated stuff should always be present in the documentation right?

[Huỳnh Trần Khanh]

At least that's my impression

[Ruben Van de Velde]

Yes, indeed - just not in the source itself

[Martin C. Martin]

Huh, when I try to use library_search in VS Code, I get unknown identifier 'library_search'

[Huỳnh Trần Khanh]

Did you import anything from mathlib? If you didn't then library_search wouldn't be present!

[Huỳnh Trần Khanh]

Please import anything from mathlib.

[Martin C. Martin]

Huỳnh Trần Khanh said:

Please import anything from mathlib.

Success! Thank you.

[Anne Baanen]

Ruben Van de Velde said:

One issue with grep is that many theorems about additive groups (etc) are written only in multiplicative form, and to_additive translates them automatically

I have mostly moved from grep (rg really) to the mathlib docs search box. It's not quite as precise but including autogenerated declarations and the limited amount of fuzzy matching really does give it some advantages.