## Stream: maths

### Topic: How to manipulate zmod and its field structure?

#### Ryan Lahfa (May 24 2020 at 08:36):

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 (May 24 2020 at 09:06):

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

#### Ryan Lahfa (May 24 2020 at 09:09):

It seems to fix my last step, indeed

#### Kevin Buzzard (May 24 2020 at 09:12):

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

Thanks !

#### Chris Hughes (May 24 2020 at 17:51):

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.

Last updated: May 14 2021 at 20:13 UTC