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. T
    The Mathematical Components team

Maintainers

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

Sources

mathcomp-2.2.0.tar.gz
sha256=e7e8f3ebfebae10fd290a63fffdbe311d32df7eebc2e66777e194269e72697f5

Description

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

Tags

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

Published: 17 Jan 2024

Dependencies (1)

  1. coq-mathcomp-solvable = version

Dev Dependencies

None

Used by (10)

  1. coq-infotheo >= "0.0.7" & < "0.1.1" | >= "0.5.1" & != "0.6.1" & < "0.7.6"
  2. coq-mathcomp-abel
  3. coq-mathcomp-analysis >= "0.3.13" & < "0.5.0" | >= "0.5.2" & != "0.5.4"
  4. coq-mathcomp-apery
  5. coq-mathcomp-cad
  6. coq-mathcomp-character = "2.2.0"
  7. coq-mathcomp-odd-order = "1.13.0"
  8. coq-mathcomp-real-closed >= "1.1.3"
  9. coq-mathcomp-sum-of-two-square >= "1.0.1"
  10. coq-monae >= "0.4.5" & < "0.7.2"

Conflicts

None