Zulip Chat Archive

Stream: new members

Topic: residue class


view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 20 2020 at 17:59):

k % n?

view this post on Zulip Johan Commelin (Mar 20 2020 at 17:59):

Or (k : zmod n)

view this post on Zulip Johan Commelin (Mar 20 2020 at 17:59):

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

view this post on Zulip orlando (Mar 20 2020 at 18:00):

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

view this post on Zulip 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!

view this post on Zulip 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. ...

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip 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?

view this post on Zulip Brian Jiang (Mar 22 2020 at 17:48):

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

view this post on Zulip 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 Z/nZ\mathbb{Z}/n\mathbb{Z}, and this would automatically inherit a group structure.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:51):

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

view this post on Zulip Brian Jiang (Mar 22 2020 at 21:52):

on my own, if possible

view this post on Zulip Brian Jiang (Mar 22 2020 at 21:55):

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

view this post on Zulip Brian Jiang (Mar 22 2020 at 21:55):

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

view this post on Zulip Brian Jiang (Mar 22 2020 at 22:05):

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

view this post on Zulip 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

view this post on Zulip Brian Jiang (Mar 22 2020 at 22:05):

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

view this post on Zulip 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