## Stream: Is there code for X?

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

#### 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.

#### Johan Commelin (Jan 29 2021 at 14:16):

zmod n

#### Johan Commelin (Jan 29 2021 at 14:17):

O wait, maybe I misunderstood.

#### Johan Commelin (Jan 29 2021 at 14:17):

Do you mean "module" or "modulo"?

#### Johan Commelin (Jan 29 2021 at 14:17):

Otherwise, ideal.span {n}?

#### Jose Certiolo (Jan 29 2021 at 14:19):

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

#### 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