residue class

Stream: new members

[Brian Jiang]

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]

k % n?

[Johan Commelin]

Or (k : zmod n)

[Johan Commelin]

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

[orlando]

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

[Brian Jiang]

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]

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]

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]

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

[Brian Jiang]

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

[Brian Jiang]

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

[Kevin Buzzard]

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]

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]

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]

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

[Brian Jiang]

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]

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

[Brian Jiang]

on my own, if possible

[Brian Jiang]

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

[Brian Jiang]

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

[Brian Jiang]

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

[Ryan Lahfa]

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]

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

[Brian Jiang]

@Ryan Lahfa : what does the finite cardinal do?