Zmod as field

Stream: mathlib4

[chris477]

Hi! I’m just starting out with lean4 and want to use it to verify the correctness of some algorithms solving polynomial equations over prime fields.

I wanted to start out proving that the equation „a*x+b=0“ can be solved by „x=-b/a“. But I’m having problems getting lean4 to understand that I’m dealing with a field and thus division exists if the modulus is prime.

I also couldn’t find a place in mathlib where it states that it is a field if the modulus is a prime.

Is this at all the right approach? I will later need the correspondence to Z because that is what most of the special cases the algorithm can solve is about.

Thanks a lot for your help!

[Yaël Dillies]

Hey! :wave: This is a great question to ask loogle about:

[Yaël Dillies]

@loogle Field (ZMod _)

[loogle]

:search: ZMod.instField, ZMod.instField.congr_simp

[Yaël Dillies]

As you see by clicking the link, you need the p.Prime hypothesis to be wrapped in docs#Fact. This is because docs#Nat.Prime is not an instance, and therefore cannot be used directly in typeclass search.

[chris477]

Ah, it looks like I have to improve my loogling skills, I was only looking at Data.ZMod and not Algebra.Field.ZMod

I think I did add the Fact but I think I also need to import that module or at least use the theorems from there.

[Yaël Dillies]

If your computer can withstand it, you can try working with import Mathlib at the top of your file. This way, you won't miss any instance

[chris477]

I’ll try, thanks!