Zulip Chat Archive

Stream: maths

Topic: order of zmod n


view this post on Zulip Guy Leroy (Aug 02 2018 at 10:40):

Hi, I'm trying to find the order of zmod n.
Chris helped me and wrote this code:

instance (n : nat) : pos_nat (nat.succ n) := ⟨nat.succ_pos _⟩
instance : fintype (units (zmod 5)) := sorry
instance : decidable_eq (units (zmod 5)) :=
λ x y, decidable_of_iff _ ⟨ units.ext, λ _,by simp *⟩
#eval @order_of (units (zmod 5)) _ _ _ ⟨(2 : zmod 5), 2⁻¹, rfl, rfl⟩

However the eval command sends the error "units.fintype: trying to evaluate sorry" presumably because we didn't prove instance : fintype (units (zmod 5)). So I guess my question is how can I prove the latter?

view this post on Zulip Kenny Lau (Aug 02 2018 at 10:49):

MWE please

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:49):

I think Chris said that units R is not just the subtype of R -- to construct a term of type units R you actually need to give both u and its inverse v. So you will need to prove some lemma (which might be already there) saying that there's an injection from units R to R, and then convince lean that a subtype of a fintype is a fintype.

To look for the injection from units R into R I would find where units are defined and then look at the code written shortly afterwards to see if there's anything useful. Then one might hope that all the rest is there already.

view this post on Zulip Kenny Lau (Aug 02 2018 at 10:50):

no, the subtype of a fintype is not a fintype. that's why you can create a fintype by a surjection but not by an injection

view this post on Zulip Kenny Lau (Aug 02 2018 at 10:50):

(but you can do various things if you have a finset of R that contains all the units, such as finset.attach)

view this post on Zulip Kenny Lau (Aug 02 2018 at 10:51):

and the injection is just units.val

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:52):

no, the subtype of a fintype is not a fintype.

Wait what? Even when everything is decidable?

view this post on Zulip Kenny Lau (Aug 02 2018 at 10:52):

if it's decidable then it's ok

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:53):

I don't know if decidability is proved, but for a in Zmod n I can decide if it's a unit or not. @Chris Hughes do you know if this needs doing, or is it already done?

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:56):

@Guy Leroy Chris suggests you prove an equiv between units (zmod n) and the nats between 0 and n-1 which are coprime to n. That would do it.

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 10:57):

Oh Ellen just messaged me, she's sitting next to me. I can't believe I'm in a room full of people all talking to each other online. Guy is about 4 metres from me. Is this how kids work nowadays?

view this post on Zulip Guy Leroy (Aug 02 2018 at 10:58):

Thanks for the answers!

view this post on Zulip Scott Morrison (Aug 02 2018 at 10:59):

@Kevin Buzzard just wait until they get the neural implants...

view this post on Zulip Kenny Lau (Aug 02 2018 at 11:00):

kids these days, only focussing on their laptops instead of on their newspapers

view this post on Zulip Patrick Massot (Aug 02 2018 at 11:12):

I'm pretty surprised they gathered in the same room. Where I studied, all freely accessible computer rooms disappeared because students stopped using them when internet reached the student housing 15 years ago.

view this post on Zulip Kenny Lau (Aug 02 2018 at 11:12):

they're doing UROP

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 11:35):

I force them to come in :-) In fact I don't even know why we're meeting in the computer room -- everyone brings their own computers.


Last updated: May 12 2021 at 07:17 UTC