API for Z/(n) = zmod n

Stream: Is there code for X?

[Hanting Zhang]

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]

I usually have mathlib open in vscode and use file search

[Mario Carneiro]

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]

do we know that Z is a PID?

[Mario Carneiro]

ah, it's a euclidean_domain

[Johan Commelin]

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]

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