package coq-mathcomp-algebra

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

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.12.0.tar.gz
sha256=a57b79a280e7e8527bf0d8710c1f65cde00032746b52b87be1ab12e6213c9783

Description

This library contains definitions and theorems about discrete (i.e. with decidable equality) algebraic structures : ring, fields, ordered fields, real fields, modules, algebras, integers, rational numbers, polynomials, matrices, vector spaces...

Tags

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

Published: 26 Nov 2020

Dependencies (1)

  1. coq-mathcomp-fingroup = version

Dev Dependencies

None

Used by (33)

  1. coq-addition-chains
  2. coq-algorand
  3. coq-bits >= "1.1.0"
  4. coq-coqeal >= "1.0.5" & < "1.1.1" | >= "2.0.0"
  5. coq-coqeal-theory
  6. coq-fcsl-pcm >= "1.8.0"
  7. coq-formalv-check_range < "1.1.0"
  8. coq-formalv-prim63_mathcomp < "1.1.0"
  9. coq-formalv-time < "1.1.0"
  10. coq-fourcolor >= "1.2.3"
  11. coq-fourcolor-reals
  12. coq-gaia
  13. coq-gaia-numbers
  14. coq-gaia-stern
  15. coq-graph-theory = "0.9" | >= "0.9.2"
  16. coq-hanoi
  17. coq-htt >= "1.3.0"
  18. coq-htt-core
  19. coq-infotheo >= "0.2.2" & < "0.3.4" | >= "0.5.1" & < "0.6.1"
  20. coq-mathcomp-abel
  21. coq-mathcomp-algebra-tactics
  22. coq-mathcomp-analysis >= "0.3.5" & < "0.5.0" | >= "0.5.2" & < "0.5.4"
  23. coq-mathcomp-apery
  24. coq-mathcomp-cad
  25. coq-mathcomp-classical
  26. coq-mathcomp-multinomials >= "1.4"
  27. coq-mathcomp-real-closed >= "1.1.2"
  28. coq-mathcomp-solvable = "1.12.0"
  29. coq-mathcomp-sum-of-two-square >= "1.0.1"
  30. coq-mathcomp-word
  31. coq-mathcomp-zify
  32. coq-monae >= "0.2.2" & < "0.4" | >= "0.4.5" & < "0.7.0"
  33. coq-robot

Conflicts

None