package coq-mathcomp-field

  1. Overview
  2. No Docs
Mathematical Components Library on Fields

Install

Dune Dependency

math-comp.github.io Edit opam file Versions (21)

Authors

  1. J
    Jeremy Avigad <>
  2. A
    Andrea Asperti <>
  3. S
    Stephane Le Roux <>
  4. Y
    Yves Bertot <>
  5. L
    Laurence Rideau <>
  6. E
    Enrico Tassi <>
  7. I
    Ioana Pasca <>
  8. G
    Georges Gonthier <>
  9. S
    Sidi Ould Biha <>
  10. C
    Cyril Cohen <>
  11. F
    Francois Garillot <>
  12. A
    Alexey Solovyev <>
  13. R
    Russell O'Connor <>
  14. L
    Laurent Théry <>
  15. A
    Assia Mahboubi <>

Maintainers

  1. M
    Mathematical Components <mathcomp-dev@sympa.inria.fr>

Sources

mathcomp-1.9.0.tar.gz
sha256=fe3d157a4db7e96f39212f76e701a7fc1e3f125c54b8c38f06a6a387eda61c96

Description

This library contains definitions and theorems about field extensions, galois theory, algebraic numbers, cyclotomic polynomials...

Tags

keyword:algebra keyword:field keyword:small scale reflection keyword:mathematical components keyword:odd order theorem logpath:mathcomp.field

Published: 28 May 2019

Dependencies (1)

  1. coq-mathcomp-solvable = "1.9.0"

Dev Dependencies

None

Used by (13)

  1. coq-geocoq-pof < "2.5.0"
  2. coq-infotheo < "0.0.7" | >= "0.5.1" & < "0.6.1"
  3. coq-libvalidsdp >= "0.6.0" & < "1.0.0"
  4. coq-mathcomp-abel
  5. coq-mathcomp-analysis >= "0.2.2" & < "0.3.1" | >= "0.3.13" & < "0.5.0" | >= "0.5.2" & != "0.5.4"
  6. coq-mathcomp-apery
  7. coq-mathcomp-cad
  8. coq-mathcomp-character = "1.9.0"
  9. coq-mathcomp-odd-order = "1.13.0"
  10. coq-mathcomp-real-closed >= "1.0.3" & < "1.1.1" | >= "1.1.3"
  11. coq-mathcomp-sum-of-two-square >= "1.0.1"
  12. coq-monae >= "0.4.5" & < "0.7.0"
  13. coq-validsdp < "1.0.0"

Conflicts

None