Paket: libcoq-mathcomp-real-closed (2.0.0-1 och andra)

[ Källkod: mathcomp-real-closed  ]

Real closed fields for Mathematical Components

This library contains definitions and theorems about real closed fields for Mathematical Components. It includes a construction of the real and algebraic closure (with a proof of the fundamental theorem of algebra). The decidability of the first order theory of real closed field, through quantifier elimination is also established.

The Mathematical Components library is a coherent repository of general-purpose formalized mathematical theories for the Coq proof assistant.

Andra paket besläktade med libcoq-mathcomp-real-closed

• dep: libcoq-mathcomp-algebra-054x7 [ppc64el]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-algebra-5a639 [s390x]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-algebra-av7q1 [armhf]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-algebra-b8f33 [i386]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-algebra-q5cc3 [arm64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-algebra-rek99 [amd64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-algebra

• dep: libcoq-mathcomp-bigenough-1sq44 [arm64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-bigenough-apzb5 [ppc64el]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-bigenough-b1k46 [s390x]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-bigenough-ioid3 [amd64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-bigenough-ldce0 [i386]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-bigenough-zs1j0 [armhf]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-bigenough

• dep: libcoq-mathcomp-field-qto61 [ppc64el]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-field-rmnb8 [amd64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-field-why37 [i386]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-field-xwkm8 [s390x]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-field-y9vf9 [arm64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-field-zid64 [armhf]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-field

• dep: libcoq-mathcomp-ssreflect-2doc4 [arm64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• dep: libcoq-mathcomp-ssreflect-ee6d7 [s390x]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• dep: libcoq-mathcomp-ssreflect-iyvz0 [ppc64el]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• dep: libcoq-mathcomp-ssreflect-rr6p1 [armhf]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• dep: libcoq-mathcomp-ssreflect-v1az1 [amd64]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• dep: libcoq-mathcomp-ssreflect-vtcb9 [i386]

  virtuellt paket som tillhandahålls av libcoq-mathcomp-ssreflect

• sug: ocaml-findlib

  management tool for OCaml libraries

Hämta libcoq-mathcomp-real-closed

Hämtningar för alla tillgängliga arkitekturer

Arkitektur	Version	Paketstorlek	Installerad storlek	Filer
amd64	2.0.0-1+b1	2.352,4 kbyte	9.905,0 kbyte	[filförteckning]
arm64	2.0.0-1+b1	2.352,7 kbyte	9.905,0 kbyte	[filförteckning]
armhf	2.0.0-1+b2	2.352,3 kbyte	9.899,0 kbyte	[filförteckning]
i386	2.0.0-1+b1	2.352,2 kbyte	9.899,0 kbyte	[filförteckning]
ppc64el	2.0.0-1+b1	2.352,2 kbyte	9.905,0 kbyte	[filförteckning]
s390x	2.0.0-1+b1	2.352,9 kbyte	9.905,0 kbyte	[filförteckning]