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. Z/nZ\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):


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

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