Elements of finite fields of char 2 are squares

Stream: Is there code for X?

[Michael Stoll]

Is this in mathlib?

lemma is_square_of_char_two {F : Type*} [field F] [fintype F] (hF : ring_char F = 2) (a : F) : is_square a := ...

(probably field F is stronger than necessary).

[Adam Topaz]

Do we not know that finite fields are perfect? I thought I saw that in mathlib at some point.

[Reid Barton]

I thought so too but can't find it

[Adam Topaz]

We certainly have Frobenius as a ring hom, which is injective hence surjective since things are finite. It should be easy enough to prove.

[Michael Stoll]

I guess the most direct way is to use a ^ (#F - 1) = 1 (for nonzero a) to write down a square root explicitly.

[Adam Topaz]

import field_theory.finite.basic

variables (p : ℕ) [fact (nat.prime p)]
variables (F : Type*) [field F] [fintype F] [char_p F p]

lemma frobenius_bijective : function.bijective (frobenius F p) :=
begin
  rw ← fintype.injective_iff_bijective,
  exact frobenius_inj F p,
end

lemma exists_pow (x : F) : ∃ y : F, y^p = x :=
(frobenius_bijective p F).surjective x

[Alex J. Best]

Slightly annoying that the definition of square is the opposite of that of surjective Edit: golf time

import field_theory.finite.basic

lemma a {K : Type*} [fintype K] [comm_ring K] [is_reduced K]  [char_p K 2] (a : K) : is_square a :=
exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) $
  ((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj K 2, rfl⟩).surjective a

[Michael Stoll]

This gives me

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  ?m_1 b

[Michael Stoll]

@Damiano Testa might be interested in this topic, too.

[Alex J. Best]

That's very strange, you mean exactly the same code in a new file gives you an error?

[Michael Stoll]

Hm, it works in a fresh file. I'll check...

[Michael Stoll]

OK, I must have done something wrong. I copied it again, and now it works.

[Damiano Testa]

Seems like I missed out on some finite field fun!