## Stream: new members

### Topic: residue class

#### Brian Jiang (Mar 20 2020 at 17:54):

How would you define a reduced residue class module n in lean? After defining it I also want to be able to multiply the generic elements of the residue class together (part of a proof for Euler's theorem)

#### Johan Commelin (Mar 20 2020 at 17:59):

k % n?

#### Johan Commelin (Mar 20 2020 at 17:59):

Or (k : zmod n)

#### Johan Commelin (Mar 20 2020 at 17:59):

Note that Euler's theorem was just added to mathlib this week

#### orlando (Mar 20 2020 at 18:00):

In mathlib, zmod is in the file " data " !

#### Brian Jiang (Mar 20 2020 at 18:05):

thanks! I'm just trying to prove it myself as an exercise. Johan Commelin can you please clarify how what you wrote gets the desired result? I want a set of numbers that are congruent to all values < n that don't share a common factor with n. Thanks!

#### Johan Commelin (Mar 20 2020 at 18:11):

There are various ways to approach this.

1. units (zmod n)
2. { k : nat | k < n \and k.coprime n }
3. (finset.range n).filter \$ assume k, k.coprime n
4. ...

#### Kevin Buzzard (Mar 20 2020 at 18:15):

Brian Jiang said:

I want a set of numbers that are congruent to all values < n that don't share a common factor with n. Thanks!

The issue is that in Lean there are multiple ways to construct such a collection, and the best way will probably depend on what you want to do with it. It's like asking the best way to write a computer program which stores a graph -- there are many ways, and the best way depends on what you want to do with the graphs you store.

#### Brian Jiang (Mar 22 2020 at 17:47):

if I define the residue class as follows:
def reduced_residue_class (n: nat):={ k : nat | k < n \and k.coprime n }

#### Brian Jiang (Mar 22 2020 at 17:48):

is there a way I can write a theorem regarding the number of elements in this set?

#### Brian Jiang (Mar 22 2020 at 17:48):

I would also like to take out elements from this set and multiply them together

#### Kevin Buzzard (Mar 22 2020 at 21:35):

Your definition is a slightly artificial way to think about this concept. The naturals already have a multiplication on them, and you are proposing defining another one. Mathematically a more natural way to do this would be to define your set to be the units of the ring $\mathbb{Z}/n\mathbb{Z}$, and this would automatically inherit a group structure.

#### Kevin Buzzard (Mar 22 2020 at 21:36):

If you want to roll your own then you will have to prove that if a and b are coprime to n then so is their product.

#### Kevin Buzzard (Mar 22 2020 at 21:47):

If you want to use mathlib's pre-rolled repesentation of this type then you have access to theorems like this:

import data.zmod.basic

example (n : ℕ+) : units (zmod n) ≃ {x : zmod n // nat.coprime x.val n} :=
zmod.units_equiv_coprime


#### Brian Jiang (Mar 22 2020 at 21:50):

is there a way with my definition to set a variable equal to the product of all the elements in the set?

#### Brian Jiang (Mar 22 2020 at 21:51):

that is what I meant earlier by multiplication, not to show if the product of two elements is still inside the set; sorry if that wasn't clear

#### Kevin Buzzard (Mar 22 2020 at 21:51):

Are you going to roll your own, or are you going to use the inbuilt one?

#### Brian Jiang (Mar 22 2020 at 21:52):

on my own, if possible

#### Brian Jiang (Mar 22 2020 at 21:55):

also, is there a way to get the size of a set?

#### Brian Jiang (Mar 22 2020 at 21:55):

also, is there a way to get the size of a set?

#### Brian Jiang (Mar 22 2020 at 22:05):

my current intention is to take a reduced residue class made up of (r1, r2, ...rn)

#### Ryan Lahfa (Mar 22 2020 at 22:05):

If you prove it's finite, you can have a finite cardinal: https://leanprover-community.github.io/mathlib_docs/data/set/finite.html

#### Brian Jiang (Mar 22 2020 at 22:05):

and show that the product r1r2...rn is congruent to (ar1)(ar2)...(arn)

#### Brian Jiang (Mar 22 2020 at 22:08):

@Ryan Lahfa : what does the finite cardinal do?

Last updated: May 08 2021 at 19:11 UTC