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.

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.

A doubt. What does `Let`

mean in mathcomp? Is it a way to have notations or something? Where can I find its documentation?

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?

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

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?

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?

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

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.

What does `\is`

mean in mathcomp?

Is it part of some LaTeX input method?

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