## Stream: new members

### Topic: How to find nat theorms in mathlib?

#### Martin C. Martin (Jul 28 2022 at 14:32):

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 (Jul 28 2022 at 14:36):

Have you tried the library_search tactic?

#### Huỳnh Trần Khanh (Jul 28 2022 at 14:36):

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 (Jul 28 2022 at 14:39):

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 (Jul 28 2022 at 14:41):

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 (Jul 28 2022 at 14:41):

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 (Jul 28 2022 at 14:45):

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

#### Huỳnh Trần Khanh (Jul 28 2022 at 14:45):

At least that's my impression

#### Ruben Van de Velde (Jul 28 2022 at 14:46):

Yes, indeed - just not in the source itself

#### Martin C. Martin (Jul 28 2022 at 15:16):

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

#### Huỳnh Trần Khanh (Jul 28 2022 at 15:20):

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

#### Martin C. Martin (Jul 28 2022 at 15:29):

Huỳnh Trần Khanh 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.