gcd

Stream: new members

[Kevin Lacker]

new navigating-the-docs question. I'm looking for where gcd is defined. search leads me to https://github.com/leanprover-community/mathlib/blob/5fd2037/src/data/nat/gcd.lean#L162 which has a comment saying, here is where gcd is defined. however, there doesn't actually seem to be a definition here? it only imports one file, https://github.com/leanprover-community/mathlib/blob/5fd2037/src/data/nat/basic.lean , but that file doesn't mention "gcd" at all. 1/ where is gcd defined, and 2/ what is the right way for me to discover this for myself

[Bryan Gin-ge Chen]

It's defined in core: docs#nat.gcd

If you type nat.gcd into the search window and wait (don't hit "search"!) then choose the first option, it should take you to this declaration.

[Bryan Gin-ge Chen]

In emacs it should be possible to peek / navigate to the definition of nat.gcd, which is another way of finding out where any given definition is.

[Kevin Lacker]

so everything under that "init" directory is automatically imported?

[Bryan Gin-ge Chen]

Yep, unless you put prelude at the top of your file.