## Stream: math-comp users

### Topic: Learning finite fields with mathcomp

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

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

Thanks.

#### 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?

#### Julin S (Mar 03 2023 at 04:28):

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?

#### Laurent Théry (Mar 03 2023 at 06:08):

`unitRingType` is a ring where some elements have an inverse, `fieldType`is 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.
``````

#### 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

#### 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!

#### Julin S (Mar 03 2023 at 16:28):

Laurent Théry said:

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

Thanks! I got this as well.

#### Julin S (Mar 03 2023 at 16:32):

What does `\is` mean in mathcomp?

#### Julin S (Mar 03 2023 at 16:32):

Is it part of some LaTeX input method?

#### 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