order of one in zmod

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is this lemma already in mathlib? I could not find it. Thanks!

import group_theory.order_of_element

lemma zmod.add_order_of_one {n : ℕ} (n0 : 0 < n) : add_order_of (1 : zmod n) = n := sorry

[Damiano Testa]

Maybe, because of the definitions it also holds for n = 0.

[Johan Commelin]

I can't find it.

[Damiano Testa]

Johan, thanks for confirming! It seems that there is little API for (add_)order_of_element in general, besides what is in the file where they are defined. In particular, even the relationship between additive order of 1 in a semiring and its interactions with the various chars seems not in mathlib.

[Damiano Testa]

I do not dislike this proof, but can someone find a more direct argument?

lemma char_p_eq_add_order_of_one (R) [semiring R] : char_p R (add_order_of (1 : R)) :=
⟨λ n, by rw [← nat.smul_one_eq_coe, add_order_of_dvd_iff_nsmul_eq_zero]⟩

lemma zmod.add_order_of_one (n : ℕ) : add_order_of (1 : zmod n) = n :=
begin
  cases zmod.char_p n with cp,
  cases char_p_eq_add_order_of_one (zmod n) with co,
  exact nat.dvd_right_iff_eq.mp (λ a, by rw [← cp, ← co]),
end

[Yaël Dillies]

Don't we have a lemma that if char_p R a and char_p R b then a = b?

[Damiano Testa]

Good point, I do not know!

[Damiano Testa]

like char_p injective, or something?

[Yaël Dillies]

char_p.unique I'd say.

[Damiano Testa]

docs#char_p.eq?

[Damiano Testa]

Thanks a lot!

[Yaël Dillies]

Also, you could generalize to anything coprime with n, and then prove the general statement that add_order_of a = n/gcd a n.

[Damiano Testa]

#16277