-
Notifications
You must be signed in to change notification settings - Fork 3
/
meta.yml
86 lines (68 loc) · 1.67 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
---
fullname: Grobner
shortname: grobner
organization: thery
community: false
dune: false
action: true
synopsis: Grobner basis
description: |-
A fornalisation of Grobner basis in ssreflect.
It contains one file
``grobner.v``
It defines
```coq
From mathcomp Require Import all_ssreflect all_algebra.
From SsrMultinomials Require Import ssrcomplements freeg mpoly.
From mathcomp.contrib.grobner Require Import grobner.
Print ideal.
(*
ideal =
fun (R : ringType) (n : nat) (L : seq {mpoly R[n]}) (p : {mpoly R[n]})
=>
exists t, p = sum_(i < size L) t`_i * L`_i
*)
(* it is decidable *)
Check idealfP.
(*
idealfP
: forall (R : fieldType) (n : nat) (p : {mpoly R[n]})
(l : seq {mpoly R[n]}),
reflect (ideal l p) (idealf l p)
*)
```
authors:
- name: Laurent Théry
maintainers:
- name: Laurent Théry
nickname: thery
opam-file-maintainer: [email protected]
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: '8.17 or later'
opam: '{(>= "8.17")}'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{(>= "2.1.0")}'
description: |-
[MathComp ssreflect 2.1 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{(>= "2.1.0")}'
description: |-
[MathComp algebra 2.1 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-multinomials
version: '{(>= "2.1.0")}'
description: |-
[MathComp Multinomials 2.1.0 or later](https://github.com/math-comp/multinomials)
tested_coq_opam_versions:
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
namespace: grobner
keywords:
- name: grobner basis
---