Finite fields in lean

Stream: new members

[Julin S]

Hi. I'm a noob at lean but have worked a little with coq. I wanted to get familiar with finite fields. Wished to prove basic lemmas. I guess they are already proven here but wanted to get a taste of how it feels like.

Any idea where I should start? lean3 is what I need I guess.

Saw this: https://leanprover-community.github.io/mathlib_docs/field_theory/finite/basic.html

But wasn't sure how to use this.

[Johan Commelin]

@Julin S Could you please be more precise? Do you have a maths statement in mind that you would like to formalize?

[Julin S]

@Johan Commelin Basic things. I'm still only learning about finite fields.

I was hoping to start with 'order of a finite field is always a positive power of a prime.'

[Johan Commelin]

Ok. Do you think you can write that statement in Lean? Just give it a shot, and we can give hints if you get stuck.

[Julin S]

Is there some library that I can use?

import field_theory.basic gave error.

But import topology.basic (as mentioned in the manual) had no errors.

[Julin S]

But on the other hand, found a definition of field here: https://github.com/leanprover-community/lftcm2020/blob/f7992fe816d7b3df81efb7ad448a30653d5c0111/src/solutions/wednesday/algebraic_hierarchy.lean

Would that be better?

[Julin S]

Oh, wait. Sounds like I got an installation issue.. Let me try fixing that.

[Johan Commelin]

After you have a working setup

import field_theory.finite.basic

should work

[Julin S]

How can I get the order of a finite field?

I sort of randomly typed this up:

theorem foo: {K:Type*} {n:ℕ} [fact p.prime] (f:field K) : (order f) = pow p n

[Julin S]

Does fact serve the same purpose as implicit arguments? Or is there something more to it?

[Julin S]

And Type* denotes the type of all types, right?

[Julin S]

Or could this be better?

theorem foo: {A:Type} {n:ℕ} [fact p.prime] (f:field A) := f.card = pow p n

[Junyan Xu]

docs#finite_field.card' is how it's stated in mathlib.

[Kevin Buzzard]

(deleted)

[Gareth Ma]

Julin S said:

Or could this be better?

theorem foo: {A:Type} {n:ℕ} [fact p.prime] (f:field A) := f.card = pow p n

Try to step back and see what what you typed says. In English / maths terms, you want to express "A field has prime power order" or equivalently "Given a field, there exists a prime power equalling to the field's order", so you shouldn't be supplying the p or n. Instead, you look at the theorem in mathlib, which only takes a field as argument and states that there exists p and n such that etc.

[Kevin Buzzard]

Currently this says something close to "for all fields A and primes p and naturals n, the size of A is p^n" (but it doesn't even say that right now, for several other reasons). You might want to start off with something simpler if you've not used lean at all before

[Julin S]

Yeah, I'm completely new to lean.

[Julin S]

A doubt: What's the difference between ℕ and ℕ+? Is it that ℕ+ only has positive ℕ?

Tried:

#check (0:ℕ+)

and that gave:

failed to synthesize type class instance for
⊢ has_zero ℕ+

[Julin S]

Thanks.

[Julin S]

Another doubt: How does one query for existing lemmas and theorem in the course of proving new theorems?

[Alex J. Best]

You can use tactic#library_search which should find if the current goal follows from an exact match of a single lemma in the library (possibly using your hypotheses).