Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 02 2021 at 05:29):

I usually have mathlib open in vscode and use file search

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 02 2021 at 05:35):

do we know that Z is a PID?

view this post on Zulip Mario Carneiro (Jan 02 2021 at 05:36):

ah, it's a euclidean_domain

view this post on Zulip 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 > #)

view this post on Zulip 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