# Zulip Chat Archive

## Stream: general

### Topic: Modular arithmetic

#### Harrison Grodin (Dec 16 2019 at 20:37):

I'm attempting to define a type (of a given size) which respects modular arithmetic - i.e. $\mathbb{Z} / n\mathbb{Z}$. I assume this is meant to be done via `quot`

(or `quotient`

?), but I can't quite figure it out. Am I on the right track here? (Or is this built in somewhere?)

#### Johan Commelin (Dec 16 2019 at 20:39):

(We have such a type in mathlib. I don't know if that is what you mean with "built in".) `quot`

is one option. The other is to build a type with `n`

elements, and put the algebraic structure on such a type.

#### Joe (Dec 16 2019 at 20:40):

I remember there is a tutorial called Zmod37.lean, which might be what you need.

#### Patrick Massot (Dec 16 2019 at 20:56):

https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean

#### Patrick Massot (Dec 16 2019 at 20:58):

#### Patrick Massot (Dec 16 2019 at 20:58):

Note this is a tutorial file, not the actual mathlib version of Z/n

#### Patrick Massot (Dec 16 2019 at 20:58):

Which is at https://github.com/leanprover-community/mathlib/blob/master/src/data/zmod/basic.lean

Last updated: Dec 20 2023 at 11:08 UTC