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

Stream: Is there code for X?

[Jose Certiolo]

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]

zmod n

[Johan Commelin]

O wait, maybe I misunderstood.

[Johan Commelin]

Do you mean "module" or "modulo"?

[Johan Commelin]

Otherwise, ideal.span {n}?

[Jose Certiolo]

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

[Johan Commelin]

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