# Zulip Chat Archive

## 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

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

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