# Zulip Chat Archive

## Stream: general

### Topic: Field of 4 elements

#### Kenny Lau (Feb 22 2019 at 22:17):

Does the field of 4 elements have its place in mathlib? I am using it in my little project as a ring that is not generated by 1, and the decidability was quite useful; if I PR my use case to mathlib, do I need to replace it by a more "regular" ring such as ZxZ or Z[X]?

#### Kenny Lau (Feb 22 2019 at 22:20):

@[derive decidable_eq] inductive F4 : Type | z | o | a | b namespace F4 instance : fintype F4 := { elems := {z, o, a, b}, complete := λ x, by cases x; simp } def add : F4 → F4 → F4 | z x := x | x z := x | o o := z | o a := b | o b := a | a o := b | a a := z | a b := o | b o := a | b a := o | b b := z def mul : F4 → F4 → F4 | z x := z | x z := z | o x := x | x o := x | a a := b | a b := o | b a := o | b b := a def inv : F4 → F4 | z := z | o := o | a := b | b := a instance : discrete_field F4 := by refine { add := add, zero := z, neg := id, mul := mul, one := o, inv := inv, has_decidable_eq := F4.decidable_eq, .. }; tactic.exact_dec_trivial end F4

#### Chris Hughes (Feb 22 2019 at 22:50):

You can prove `discrete_field`

constructively for `adjoin_root`

using euclidean division I guess, or just for finite fields using a search.

#### Kevin Buzzard (Feb 22 2019 at 23:09):

I think there's a place in mathlib for the field with q elements, and one could define it as the splitting field of X^q-X over Z/pZ if q is a power of p

#### Kenny Lau (Feb 22 2019 at 23:09):

yeah but specifically 4 elements

#### Mario Carneiro (Feb 22 2019 at 23:36):

insert q= 4?

#### Kenny Lau (Feb 22 2019 at 23:41):

that seems too much work for something not with that purpose

#### Mario Carneiro (Feb 22 2019 at 23:42):

but this seems like a lot of case analysis for a more abstract thing

#### Mario Carneiro (Feb 22 2019 at 23:43):

If you just need to know a field with 4 elements exists, that's definitely part of a more general theorem

#### Kenny Lau (Feb 22 2019 at 23:44):

no I just want a simple ring that is not generated by 1

#### Kenny Lau (Feb 22 2019 at 23:44):

simple as in not complicated

#### Mario Carneiro (Feb 22 2019 at 23:44):

ring? How about `zmod 2 x zmod 2`

#### Mario Carneiro (Feb 22 2019 at 23:45):

or `rat`

or `real`

#### Kenny Lau (Feb 22 2019 at 23:48):

and you need to be able to prove that it is not generated by 1

#### Mario Carneiro (Feb 22 2019 at 23:48):

sqrt 2 is not in Q

#### Kenny Lau (Feb 22 2019 at 23:50):

sqrt 2 is easier than 1/2?

#### Mario Carneiro (Feb 22 2019 at 23:51):

I wasn't sure which "generated" you meant. 1/2 works too

#### Mario Carneiro (Feb 22 2019 at 23:51):

I recall Kevin looking for a short proof that 1/2 is not an integer. I think noting it has denominator 2 works

#### Mario Carneiro (Feb 22 2019 at 23:52):

or 0 < 1/2 <1

#### Kenny Lau (Feb 22 2019 at 23:52):

lemme try that later

#### Kevin Buzzard (Feb 22 2019 at 23:59):

Q is not generated by 1 because Z is a subring and 1/2 is not an integer

#### Kevin Buzzard (Feb 23 2019 at 00:01):

The complexes are not generated by 1 because the reals are a subring and i is not real, maybe that's easier

#### Kenny Lau (Feb 23 2019 at 00:01):

yeah but are they in mathlib?

#### Mario Carneiro (Feb 23 2019 at 00:03):

We usually don'r state such theorems explicitly, but sqrt 2 not in Q is an exception

#### Kenny Lau (Feb 23 2019 at 00:03):

oh brilliant

#### Mario Carneiro (Feb 23 2019 at 00:03):

i not real also sound like a good candidate

#### Kevin Buzzard (Feb 23 2019 at 00:03):

You mean the fact that the reals are a subring? Everything else is. Why do you want examples anyway? It's theorems we need :-)

#### Mario Carneiro (Feb 23 2019 at 00:04):

That's my point. Most of these are just "examples" so they don't go in mathlib

#### Kevin Buzzard (Feb 23 2019 at 00:04):

Lack of examples makes maths UG example sheets harder to do

#### Mario Carneiro (Feb 23 2019 at 00:04):

There are a few cases of examples that are actually useful for theorems, and I think having simple things like this is good

#### Mario Carneiro (Feb 23 2019 at 00:05):

that's a good thing, it means the kids can't cheat :)

#### Mario Carneiro (Feb 23 2019 at 00:06):

I consider example making part of the educator's job

#### Kenny Lau (Feb 23 2019 at 01:05):

we have theorems about irrational numbers but not rational numbers?

#### Kenny Lau (Feb 23 2019 at 01:09):

thanks, sqrt 2 worked like a charm! @Mario Carneiro

#### Kenny Lau (Feb 23 2019 at 01:09):

theorem is_supported_pure {p} {s : set α} : is_supported (pure p) s ↔ p ∈ s := suffices is_supported (pure p) s → p ∈ s, from ⟨this, λ hps, ring.subset_closure ⟨p, hps, rfl⟩⟩, assume hps : is_supported (pure p) s, begin classical, have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ q, if q ∈ s then 0 else real.sqrt 2) x = ↑q, { intros x hx, refine ring.in_closure.rec_on hx _ _ _ _, { use 1, rw [lift_one, rat.cast_one] }, { use -1, rw [lift_neg, lift_one, rat.cast_neg, rat.cast_one], }, { rintros _ ⟨z, hzs, rfl⟩ _ _, use 0, rw [lift_mul, lift_of, if_pos hzs, zero_mul, rat.cast_zero] }, { rintros x y ⟨q, hq⟩ ⟨r, hr⟩, use q+r, rw [lift_add, hq, hr, rat.cast_add] } }, specialize this (of p) hps, rw [lift_of] at this, split_ifs at this, { exact h }, exfalso, exact irr_sqrt_two this end

#### Mario Carneiro (Feb 23 2019 at 01:10):

what is `is_supported pure`

?

#### Kenny Lau (Feb 23 2019 at 01:11):

def is_supported (x : free_comm_ring α) (s : set α) : Prop := x ∈ ring.closure (of '' s)

Last updated: May 13 2021 at 19:20 UTC