## Stream: new members

### Topic: working with sets

#### Brian Jiang (Mar 23 2020 at 20:14):

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

#### Brian Jiang (Mar 23 2020 at 20:15):

is there a way to get the size of this set?

#### Brian Jiang (Mar 23 2020 at 20:15):

also I would like to get the product of all elements in the set

#### Johan Commelin (Mar 23 2020 at 20:15):

Well.... Lean doesn't know yet that the set is finite...

#### Johan Commelin (Mar 23 2020 at 20:16):

Even though it's obvious.

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

This might be one reason to choose

def rsc (n : nat) : finset nat := (finset.range n).filter \$ assume k, k.coprime n


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

Then you can talk about finset.card _ afterwards

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

is there any way around this? maybe by adding an assumption that says its finite?

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

is there any way around this? maybe by adding an assumption that says its finite?

ok thanks

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

can I get the product of all elements in this set somehow?

#### Johan Commelin (Mar 23 2020 at 20:19):

also

lemma mem_rsc (n k : nat) : k \in rsc n \iff (k < n \and k.coprime n) := sorry


#### Johan Commelin (Mar 23 2020 at 20:19):

With the finset definition, the product is also easier.

#### Johan Commelin (Mar 23 2020 at 20:20):

def prod_rsc (n) : nat := (rsc n).prod id


#### Brian Jiang (Mar 23 2020 at 20:22):

what do I have to import for finset and prod?

#### Kevin Buzzard (Mar 23 2020 at 20:23):

You can't take the product until you define the multiplication.

#### Johan Commelin (Mar 23 2020 at 20:25):

Brian Jiang said:

what do I have to import for finset and prod?

algebra.big_operators

#### Brian Jiang (Mar 23 2020 at 20:33):

@Kevin Buzzard : How may I define this multiplication?

#### Brian Jiang (Mar 23 2020 at 20:34):

also, would it be possible to define another set that has all the values of rsc n  scaled by a factor of a?

#### Kevin Buzzard (Mar 23 2020 at 20:51):

Well you can do regular multiplication and then reduce mod n -- but then you have to prove that the result is coprime to n. If you want to roll your own then you will have to do work before you can even start multiplying.

If you want to learn how to prove theorems in Lean than you could try working on the natural number game.

Last updated: May 17 2021 at 22:15 UTC