Zulip Chat Archive

Stream: new members

Topic: working with sets


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

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:15):

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

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:15):

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

view this post on Zulip Johan Commelin (Mar 23 2020 at 20:15):

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

view this post on Zulip Johan Commelin (Mar 23 2020 at 20:16):

Even though it's obvious.

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

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

Then you can talk about finset.card _ afterwards

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:17):

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

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:17):

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

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:18):

ok thanks

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:18):

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

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

view this post on Zulip Johan Commelin (Mar 23 2020 at 20:19):

With the finset definition, the product is also easier.

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

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

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

what do I have to import for finset and prod?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 20:23):

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

view this post on Zulip Johan Commelin (Mar 23 2020 at 20:25):

Brian Jiang said:

what do I have to import for finset and prod?

algebra.big_operators

view this post on Zulip Brian Jiang (Mar 23 2020 at 20:33):

@Kevin Buzzard : How may I define this multiplication?

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

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