Modular arithmetic

Stream: general

[Harrison Grodin]

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]

(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]

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

[Patrick Massot]

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

[Patrick Massot]

Or https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fcors-anywhere.herokuapp.com%2Fhttps%3A%2F%2Fraw.githubusercontent.com%2Fleanprover-community%2Fmathlib%2Fmaster%2Fdocs%2Ftutorial%2FZmod37.lean to see it online.

[Patrick Massot]

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

[Patrick Massot]

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