How to manipulate zmod and its field structure?

Stream: maths

[Ryan Lahfa]

I'm trying to prove some basic example stuff:

import algebra.group.basic
import algebra.group_power
import data.zmod.basic

def aperiodic_element {M : Type} [monoid M] (a : M) :=
  ∃n : ℕ, a^n = a^(n+1)

def aperiodic_monoid (M : Type) [monoid M] :=
  ∀x : M, aperiodic_element x

-- example of multiplicative monoids of Z/(n) rings

example : aperiodic_monoid (zmod 2) := begin
  unfold aperiodic_monoid, intro x,
  unfold aperiodic_element, use 1,
  norm_num, rw pow_two,
  have possible_values : ∀ y : zmod 2, y = 0 ∨ y = 1 := dec_trivial,
  cases (possible_values x) with xz xo,
  rw xz, refl,
  rw xo, refl,
end

example : ¬(aperiodic_monoid (zmod 3)) := begin
  unfold aperiodic_monoid,
  push_neg, use 2,
  unfold aperiodic_element, push_neg,
  intros n h,
  rw pow_succ at h,
  rw ← mul_one ((2: zmod 3)^n) at h, -- how to do things starting here?
  unfreezeI,
  haveI: fact (nat.prime 3) := sorry,
  haveI := zmod.field 3,
  have: ((2: zmod 3)^n ≠ 0) := sorry,
  have := mul_left_cancel' this h,
end

My problem is that for the second example, we are struggling to get a left (or right)-cancellation, because zmod is a field only if 3 is prime, so I try to inject the instance using haveI/unfreezeI, but it prevents me to rewrite the 1 properly.
I don't know if I'm doing something wrong.
set_option pp.all true does not help me as everything is "finite" and produces infinite terms

(code taken from a friend who is trying to formalize some of his work)

[Kevin Buzzard]

Do you need letI for the field instance? It's not a Prop I guess.

[Ryan Lahfa]

It seems to fix my last step, indeed

[Kevin Buzzard]

example : ¬(aperiodic_monoid (zmod 3)) := begin
  unfold aperiodic_monoid,
  push_neg, use 2,
  unfold aperiodic_element, push_neg,
  intros n h,
  rw pow_succ at h,
  rw (show (2 : zmod 3)* 2^n = 2^n + 2^n, by ring) at h,
  have : (2 : zmod 3) ^ n = 0,
  { library_search},
  haveI : fact (nat.prime 3) := by norm_num,
  refine pow_ne_zero n _ this,
  exact dec_trivial,
end

Lazy proving

[Ryan Lahfa]

Thanks !

[Chris Hughes]

Doing haveI for the field structure will cause problems because have forgets the definitions, so Lean won't know that the new field structure coincides with the old ring structure.