order of zmod n

Stream: maths

[Guy Leroy]

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?

[Kenny Lau]

MWE please

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

and the injection is just units.val

[Kevin Buzzard]

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

Wait what? Even when everything is decidable?

[Kenny Lau]

if it's decidable then it's ok

[Kevin Buzzard]

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?

[Kevin Buzzard]

@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.

[Kevin Buzzard]

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?

[Guy Leroy]

Thanks for the answers!

[Scott Morrison]

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

[Kenny Lau]

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

[Patrick Massot]

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.

[Kenny Lau]

they're doing UROP

[Kevin Buzzard]

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.