Zulip Chat Archive

Stream: new members

Topic: Finite fields in lean

Julin S (Feb 25 2023 at 05:50):

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 (Feb 25 2023 at 06:29):

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

Julin S (Feb 25 2023 at 06:58):

@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 (Feb 25 2023 at 07:00):

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 (Feb 25 2023 at 07:55):

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 (Feb 25 2023 at 07:56):

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 (Feb 25 2023 at 07:58):

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

Johan Commelin (Feb 25 2023 at 08:00):

After you have a working setup

import field_theory.finite.basic

should work

Julin S (Feb 26 2023 at 05:33):

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 (Feb 26 2023 at 05:33):

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

Julin S (Feb 26 2023 at 05:35):

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

Julin S (Feb 26 2023 at 05:41):

Or could this be better?

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

Junyan Xu (Feb 26 2023 at 05:55):

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

Kevin Buzzard (Feb 26 2023 at 06:51):


Gareth Ma (Feb 26 2023 at 11:15):

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 (Feb 26 2023 at 11:53):

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 (Feb 27 2023 at 07:07):

Yeah, I'm completely new to lean.

Julin S (Feb 27 2023 at 07:09):

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


#check (0:+)

and that gave:

failed to synthesize type class instance for
 has_zero +

Julin S (Feb 27 2023 at 16:14):


Julin S (Feb 27 2023 at 16:14):

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

Alex J. Best (Feb 27 2023 at 17:08):

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).

Last updated: Dec 20 2023 at 11:08 UTC