## Stream: Is there code for X?

### Topic: API for Z/(n) = zmod n

#### Hanting Zhang (Jan 02 2021 at 05:27):

Back again. :sweat_smile: Is there any API regarding the correspondence between the ideals of Z and zmod n? I'm searching because data.nat.totient seems to be missing a proof that totient is multiplicative, and there's already enough API for zmod and the Chinese Remainder Theorem to finish the proof, excepting this equivalence.
Anyways, in general, how do y'all search stuff up, err, quickly? Is there a better way than using the Docs and Github?

#### Mario Carneiro (Jan 02 2021 at 05:29):

I usually have mathlib open in vscode and use file search

#### Mario Carneiro (Jan 02 2021 at 05:31):

it looks like there are zero hits for ideal ℤ, but I would bet that there is a theorem that is equivalent to this without using ring theory notation in data.zmod.basic

#### Mario Carneiro (Jan 02 2021 at 05:35):

do we know that Z is a PID?

#### Mario Carneiro (Jan 02 2021 at 05:36):

ah, it's a euclidean_domain

#### Johan Commelin (Jan 02 2021 at 06:30):

In this case I would search for something about ideal and surjective.
Concerning search, I use command line tools like grep (or rg) and the search functionality in VScode (Ctrl-P > #)

#### Bryan Gin-ge Chen (Jan 02 2021 at 06:34):

(Ctrl-T is the direct shortcut for symbol search.)

Last updated: May 17 2021 at 16:26 UTC