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
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
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
Johan Commelin (Jan 02 2021 at 06:30):
In this case I would search for something about
Concerning search, I use command line tools like
rg) and the search functionality in VScode (
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