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.10.0.tar.gz
sha256=3f8a88417f3456da05e2755ea0510c1bd3fd13b13c41e62fbaa3de06be040166

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: 02 Dec 2019

Dependencies (1)

  1. coq-mathcomp-fingroup = version

Dev Dependencies

None

Conflicts

None