Zulip Chat Archive

Stream: Is there code for X?

Topic: Is there a definition of a Z-module nZ for any n?


view this post on Zulip Jose Certiolo (Jan 29 2021 at 14:16):

Hi, is there a definition of a Z-module nZ for any n? I don't seem to find any such definition, I was wondering if I needed to re-invent the wheel or rely on mathlib.

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:16):

zmod n

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:17):

O wait, maybe I misunderstood.

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:17):

Do you mean "module" or "modulo"?

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:17):

Otherwise, ideal.span {n}?

view this post on Zulip Jose Certiolo (Jan 29 2021 at 14:19):

oh thanks didn't thought ideal and module where the same definition in Lean

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:19):

ideal is defined using submodule. But if you treat it as a type, it automatically becomes a module.


Last updated: May 19 2021 at 02:10 UTC