Stream: math-comp users

Topic: Learning finite fields with mathcomp


view this post on Zulip Julin S (Mar 02 2023 at 15:48):

Hi. I'm currently taking course on abstract algebra.

Would trying to prove theorems related to finite fields using mathcomp be a good idea?

I'm somewhat familiar with coq syntax, but totally new to mathcomp.

view this post on Zulip Enrico Tassi (Mar 02 2023 at 16:54):

Then I suggest you look at https://math-comp.github.io/mcb/ before starting (at least the first half). Also see https://math-comp.github.io/ for more links to documentation. And feel free to ask here any question you might have.

view this post on Zulip Julin S (Mar 03 2023 at 04:25):

Thanks.

view this post on Zulip Julin S (Mar 03 2023 at 04:26):

A doubt. What does Let mean in mathcomp? Is it a way to have notations or something? Where can I find its documentation?

view this post on Zulip Julin S (Mar 03 2023 at 04:28):

And had been looking at https://www-sop.inria.fr/teams/marelle/advanced-coq-16/lesson5.html

Found that:

 rings with invertible elements: unitRingType
 fields: fieldType

What's the difference between these two types?

I'm still only learning algebra, but isn't field a ring where all elements except zero are invertible?

view this post on Zulip Laurent Théry (Mar 03 2023 at 06:08):

unitRingType is a ring where some elements have an inverse, fieldTypeis a ring where all non-zero elements have an inverse.

From mathcomp Require Import all_ssreflect all_algebra.
Import GRing.Theory.
Open Scope ring_scope.

Goal forall (R : unitRingType) (x : R), x \is a GRing.unit -> x * x^-1 = 1.
apply: mulrV.
Qed.

Goal forall (R : fieldType) (x : R), x != 0 -> x * x^-1 = 1.
apply: mulfV.
Qed.

view this post on Zulip Laurent Théry (Mar 03 2023 at 07:06):

Julin S said:

A doubt. What does Let mean in mathcomp? Is it a way to have notations or something? Where can I find its documentation?

here

view this post on Zulip Julin S (Mar 03 2023 at 14:52):

Laurent Théry said:

Julin S said:

A doubt. What does Let mean in mathcomp? Is it a way to have notations or something? Where can I find its documentation?

here

Oh, it's part of standard coq itself.. Thought it was specific to mathcomp. Thanks!

view this post on Zulip Julin S (Mar 03 2023 at 16:28):

Laurent Théry said:

unitRingType is a ring where some elements have an inverse, fieldTypeis a ring where all non-zero elements have an inverse.

Thanks! I got this as well.

view this post on Zulip Julin S (Mar 03 2023 at 16:32):

What does \is mean in mathcomp?

view this post on Zulip Julin S (Mar 03 2023 at 16:32):

Is it part of some LaTeX input method?

view this post on Zulip Pierre Roux (Mar 03 2023 at 16:36):

This is explained in the comment at the beggining of this file: https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v (initially part of MathComp, now integrated in Coq).
No link with LaTeX except the similar syntax.


Last updated: Jul 25 2024 at 15:02 UTC