CoRN.classes.Qclasses

CoRN.classes.Qposclasses

CoRN.util.Extract

CoRN.util.Container

CoRN.util.Qdlog

CoRN.util.Qgcd

CoRN.util.PointFree

CoRN.util.list_separates

CoRN.util.Qsums

CoRN.util.SetoidPermutation

CoRN.stdlib_omissions.N

CoRN.stdlib_omissions.P

CoRN.stdlib_omissions.Q

CoRN.stdlib_omissions.Pair

CoRN.stdlib_omissions.List

CoRN.stdlib_omissions.Z

CoRN.metric2.Classification

• • Classification of metric spaces

CoRN.metric2.StepFunction

• Step Functions

CoRN.metric2.FinEnum

• Finite Enumerations
  • Equivalence
  • Metric Space
  • Strong Hausdroff Metric

CoRN.metric2.DistanceMetricSpace

CoRN.metric2.StepFunctionMonad

• • Monad

CoRN.metric2.CompleteProduct

• • • Completion of product spaces.

CoRN.metric2.Graph

• Graphing
  • Graph and Bind

CoRN.metric2.Compact

• Compact sets
  • Bishop Compactness
  • Definition of Compact
  • Compact is Bishop Compact.
  • Bishop Compact is Compact.
  • Isomorphism
  • FinEnum distributes over Complete
  • Compact Image

CoRN.metric2.UniformContinuity

• • Uniform Continuity
    • The metric space of uniformly continuous functions
    • The category of metric spaces.

CoRN.metric2.StepFunctionSetoid

• • Step Functions over setoids
  • Equivalence
  • Common subdivision view
  • Applicative Functor

CoRN.metric2.Hausdorff

• Hausdorff Metric
  • Strong Hausdorff Metric

CoRN.metric2.Classified

CoRN.metric2.ProductMetric

• • Product Metric

CoRN.metric2.Limit

• • Limits

CoRN.metric2.Complete

• • Complete metric space
    • Regular functions
    • Cunit
    • Cjoin
    • Cmap (slow)
    • Strong Monad
    • Completion and Classification

CoRN.metric2.MetricMorphisms

CoRN.metric2.Metric

• Metric Space

CoRN.metric2.CompletePointFree

CoRN.metric2.Prelength

• • Prelength space
    • A more effictient Cmap and Cbind

CoRN.order.SemiLattice

• SemiLattice

CoRN.order.TotalOrder

• Total Order
  • Dual Total Order
  • Default meet and join.

CoRN.order.Lattice

• Lattice
  • Dual Latice

CoRN.order.PartialOrder

• Partial Order
  • Dual Order
  • Default Monotone and Antitone

CoRN.transc.MoreArcTan

• • ArcTan Series

CoRN.transc.TrigMon

• • Derivative of Tangent

CoRN.transc.SinCos

• • Basic properties

CoRN.transc.TaylorSeries

• Taylor Series
  • Definitions
  • Convergence

CoRN.transc.Pi

• • Definition of Pi
  • Properties of Pi
  • More formulas

CoRN.transc.Trigonometric

• The Trigonometric Functions

CoRN.transc.ArTanH

• Inverse Hyperbolic Tangent Function

CoRN.transc.InvTrigonom

• Inverse Trigonometric Functions
  • Definitions
    • Arcsine
    • Arccosine
    • Arctangent
  • Composition properties
    • Sine and Arcsine
    • Cosine and Arcosine
    • Tangent and Arctangent

CoRN.transc.Exponential

• Exponential and Logarithmic Functions
  • Properties of Exponential
  • Properties of Logarithm

CoRN.transc.PowerSeries

• More on Power Series
  • General results
  • Function definitions through power series

CoRN.transc.RealPowers

• Arbitrary Real Powers
  • Powers of Real Numbers
  • Power Function

CoRN.tactics.Qauto

CoRN.tactics.CornTac

CoRN.tactics.csetoid_rewrite

CoRN.tactics.DiffTactics2

CoRN.tactics.Rational

CoRN.tactics.Step

CoRN.tactics.RingReflection

CoRN.tactics.DiffTactics1

• Search tactics for reasoning in Real Analysis

CoRN.tactics.DiffTactics3

CoRN.tactics.AlgReflection

CoRN.tactics.FieldReflection

CoRN.reals.Cauchy_CReals

• The Real Number Structure
  • Injection of Q
  • Cauchy Completeness

CoRN.reals.fast.RasterizeQ

• • Rasterization

CoRN.reals.fast.CRartanh_slow

• • Area Tangens Hyperbolicus (artanh)

CoRN.reals.fast.MultivariatePolynomials

• • Multivariable polynomails

CoRN.reals.fast.CRpi

CoRN.reals.fast.ContinuousCorrect

• • Correctness of continuous functions.

CoRN.reals.fast.CRGeometricSum

• • Geometric Series

CoRN.reals.fast.CRsin

• • Sine

CoRN.reals.fast.CRball

CoRN.reals.fast.RasterQ

• • Rasters on Planes

CoRN.reals.fast.LazyNat

• Lazy Nat
  • Successor
  • Predecessor
  • Addition
  • Multiplication

CoRN.reals.fast.Integration

• Effective Integration
  • stepSample
  • StepFunctions distribute over Completion
  • Riemann-Stieltjes Integral

CoRN.reals.fast.CRln

• • Logarithm

CoRN.reals.fast.CRcos

• • Cosine

CoRN.reals.fast.CRseries

• • Specific results for series on Q
    • StreamBounds
    • ppositives
    • Qrecip_positives
    • pfactorials
    • Qrecip_factorials

CoRN.reals.fast.CRarctan_small

• • Arctangent (small)

CoRN.reals.fast.PowerBound

CoRN.reals.fast.CRpi_fast

• • Pi

CoRN.reals.fast.Plot

• Plotting

CoRN.reals.fast.CRpi_slow

• • Pi (alternate)

CoRN.reals.fast.CRIR

• • Isomorphism between CR and IR

CoRN.reals.fast.CRexp

• • Exponential
    • e

CoRN.reals.fast.Compress

• • Compression

CoRN.reals.fast.CRroot

• • Square Root

CoRN.reals.fast.CRsum

CoRN.reals.fast.CRarctan

• • Arctangent

CoRN.reals.fast.CRFieldOps

• • Strict Inequality
  • Apartness
  • Multiplication
  • Inverse

CoRN.reals.fast.AbstractIntegration

CoRN.reals.fast.CRabs

• • Absolute Value

CoRN.reals.fast.ModulusDerivative

• • Modulus of continity and derivatives.

CoRN.reals.fast.NewAbstractIntegration

CoRN.reals.fast.CRArith

• • Ring

CoRN.reals.fast.CRcorrect

• • Isomorphism between CR and Cauchy_IR
    • CR to Cauchy_IR
    • Cauchy_IR to CR
    • Functions preserved by isomorphism.

CoRN.reals.fast.CRAlternatingSum

• • Computing Alternating Series.

CoRN.reals.fast.CRpower

• • Natural Integer Powers

CoRN.reals.fast.CRGroupOps

• • Addition
  • Negation
  • Subtraction
  • Inequality
  • Maximum
  • Minimum

CoRN.reals.fast.Interval

• Intervals as a Compact Set.

CoRN.reals.fast.CRsign

• • Tactics for Inequalities

CoRN.reals.fast.CRtrans

CoRN.reals.fast.uneven_CRplus

CoRN.reals.CMetricFields

• Metric Fields

CoRN.reals.Max_AbsIR

• • Maximum, Minimum and Absolute Value
    • Maximum
    • Mininum
    • Absolute value
    • Bound of sequence
    • Functional Operators

CoRN.reals.Cesaro

CoRN.reals.CReals

• Definition of the notion of reals

CoRN.reals.Bridges_iso

CoRN.reals.Intervals

• Intervals
  • Definitions
  • Totally Bounded
  • Compact sets

CoRN.reals.OddPolyRootIR

• Roots of polynomials of odd degree
  • Monic polynomials are positive near infinity
  • Flipping a polynomial
  • Sign of a polynomial of odd degree
  • The norm of a polynomial
  • Roots of polynomials of odd degree

CoRN.reals.R_morphism

CoRN.reals.CReals1

• • Miscellaneous
    • More properties of Cauchy sequences
    • Subsequences
    • More properties of Exponentiation
    • IR has characteristic zero

CoRN.reals.RealCount

CoRN.reals.faster.ARcos

CoRN.reals.faster.ARtrans

CoRN.reals.faster.ARarctan

CoRN.reals.faster.ARbigQ

CoRN.reals.faster.ARsin

CoRN.reals.faster.ARArith

CoRN.reals.faster.ARbigD

CoRN.reals.faster.ARAlternatingSum

CoRN.reals.faster.ARQ

CoRN.reals.faster.ARpi

CoRN.reals.faster.ARroot

CoRN.reals.faster.AQmetric

CoRN.reals.faster.ARexp

CoRN.reals.faster.ARsign

CoRN.reals.faster.ApproximateRationals

CoRN.reals.faster.ARarctan_small

CoRN.reals.CPoly_Contin

• Continuity of polynomials

CoRN.reals.RealFuncts

• Continuity of Functions on Reals

CoRN.reals.Bridges_LUB

CoRN.reals.RealLists

• Lists of Real Numbers

CoRN.reals.iso_CReals

CoRN.reals.PosSeq

CoRN.reals.IVT

• Intermediate Value Theorem
  • Nested intervals
  • Bissections
  • IVT for operations
  • IVT for polynomials

CoRN.reals.Series

• Series of Real Numbers
  • Definitions
  • Power Series
  • Operations
  • Almost Everywhere
  • Convergence Criteria
  • Alternate Series
  • Important Numbers

CoRN.reals.Q_in_CReals

• On density of the image of Q in an arbitrary real number structure
  • Injection from Q to an arbitrary real number structure
  • Injection preserves Cauchy property
  • Injection of Q is dense

CoRN.reals.CSumsReals

• Sums over Reals

CoRN.reals.Q_dense

CoRN.reals.NRootIR

• Roots of Real Numbers
  • Existence of roots
  • Square root
  • More on absolute value
  • Cauchy sequences
    • Functional Operators

CoRN.reals.CauchySeq

• Real Number Structures
  • CReals axioms
  • Cauchy sequences
    • Alternative definitions
    • Inequalities of Limits
    • Equivalence of formulations of Cauchy
    • Properties of Cauchy sequences

CoRN.raster.Raster

• Rasters

CoRN.model.Zmod.ZBasics

• Basic facts on Z
  • Arithmetic over nat
  • Arithmetic over Z
  • Facts on inequalities over Z
  • Facts on the absolute value-function over Z
  • Facts on the sign-function over Z

CoRN.model.Zmod.ZGcd

• The GCD-function over Z
  • GCD over `positive'
  • GCD over Z
  • Relative primality
  • Primes

CoRN.model.Zmod.IrrCrit

• An irreducibility criterion
  • Integers modulo p
  • Integer polynomials over Fp
  • Lemmas
  • Working towards the criterion
    • Definitions
    • The criterion

CoRN.model.Zmod.Zm

• Zm
  • Zm is a CSetoid
  • Zm is a CAbGroup
  • Zm is a CRing
  • Zp is a field
    • The inverse element in Zp

CoRN.model.Zmod.ZMod

• Working modulo a positive number over Z
  • Facts on `mod'

CoRN.model.Zmod.ZDivides

• The Divides-function over Z

CoRN.model.Zmod.Cmod

• CProp-valued lemmas about 'mod'

CoRN.model.semigroups.QSpossemigroup

• • Example of a semi-group: ⟨Q⁺,(x,y) ↦ xy/2⟩

CoRN.model.semigroups.Zsemigroup

• • Examples of semi-groups: ⟨Z,+⟩ and ⟨Z,×⟩
    • ⟨Z,+⟩
    • ⟨Z,×⟩

CoRN.model.semigroups.Qsemigroup

• • Examples of semi-groups: ⟨Q,+⟩ and ⟨Q,×⟩
    • ⟨Q,+⟩
    • ⟨Q,×⟩

CoRN.model.semigroups.Qpossemigroup

• • Example of a semi-group: ⟨Q⁺,×⟩

CoRN.model.semigroups.CRsemigroup

• • Examples of semi-groups: ⟨CR,+⟩
    • ⟨CR,+⟩

CoRN.model.semigroups.Nsemigroup

• • Example of a semi-group: ⟨N,+⟩

CoRN.model.semigroups.Npossemigroup

• • Examples of semi-groups: ⟨N⁺,+⟩ and ⟨N⁺,×⟩
    • ⟨N⁺,+⟩
    • ⟨N⁺,×⟩

CoRN.model.reals.Cauchy_IR

• Cauchy Real Numbers

CoRN.model.reals.CRreal

• • Example of a real number structure: ⟨CR⟩

CoRN.model.groups.QSposgroup

• • Example of a group: ⟨Q⁺, (x,y) ↦ xy/2⟩

CoRN.model.groups.CRgroup

• • Example of a group: ⟨CR,+⟩

CoRN.model.groups.Qgroup

• • Example of a group: ⟨Q,+⟩

CoRN.model.groups.Zgroup

• • Example of a group: ⟨Z,+⟩

CoRN.model.groups.Qposgroup

• • Example of a group: ⟨Q⁺,×⟩

CoRN.model.rings.Zring

• • Example of a ring: ⟨Z,+,×⟩

CoRN.model.rings.CRring

• • Example of a ring: ⟨CR,+,*⟩

CoRN.model.rings.Qring

• • Example of a ring: ⟨Q,+,×⟩

CoRN.model.lattice.CRlattice

• • Example of a Lattice: <CR, CRle, CRmin, CRmax>

CoRN.model.metric2.L1metric

• • L1 metric for Step Functions
    • Integeral for Step Functions.
    • Example of a Metric Space <StepQ, L1Ball>

CoRN.model.metric2.Qmetric

• • Example of a Metric: <Q, Qball>

CoRN.model.metric2.LinfDistMonad

• • Completion distributes over Step Functions

CoRN.model.metric2.LinfMetricMonad

• • Linf metric for Step Functions
    • Example of a Metric Space <Step, StepFSupBall>

CoRN.model.metric2.CRmetric

• Complete Metric Space: Computable Reals (CR)

CoRN.model.metric2.IntegrableFunction

• • Example of a Complete Metric Space: IntegrableFunction

CoRN.model.metric2.BoundedFunction

• • Example of a Complete Metric Space: BoundedFunction

CoRN.model.metric2.LinfMetric

• • • Sup for Step Functions on Q.

CoRN.model.ordfields.Qordfield

• • Example of an ordered field: ⟨Q,+,×,<⟩

CoRN.model.ordfields.CRordfield

CoRN.model.monoids.Zmonoid

• • Examples of monoids: ⟨Z,+⟩ and ⟨Z,×⟩
    • ⟨Z,+⟩
    • ⟨Z,×⟩

CoRN.model.monoids.Nmonoid

• • Example of a monoid: ⟨N,+⟩

CoRN.model.monoids.freem_to_Nm

• • A morphism from a free monoid to the natural numbers

CoRN.model.monoids.Qmonoid

• • Examples of a monoid: ⟨Q,+⟩ and ⟨Q,×⟩
    • ⟨Q,+⟩
    • ⟨Q,×⟩

CoRN.model.monoids.Nposmonoid

• • Example of a monoid: ⟨N⁺,×⟩

CoRN.model.monoids.QSposmonoid

• • Example of a monoid: ⟨Q⁺, (x,y) ↦ xy/2⟩

CoRN.model.monoids.Nm_to_cycm

• • A function from the natural numbers to a cyclic monoid

CoRN.model.monoids.Nm_to_freem

• • A morphism from the natural numbers to the free setoid with one element

CoRN.model.monoids.CRmonoid

• • Examples of monoids: ⟨CR,+⟩
    • ⟨CR,+⟩

CoRN.model.monoids.Qposmonoid

• • Example of a monoid: ⟨Q⁺,×⟩

CoRN.model.totalorder.QposMinMax

• • Example of a Total Order: <Qpos, Qpos_le, Qpos_min, Qpos_max>

CoRN.model.totalorder.ZMinMax

• • Example of a Total Order: <Z, Zle, Zmin, Zmax>

CoRN.model.totalorder.QMinMax

• • Example of a Total Order: <Q, Qle, Qmin, Qmax>

CoRN.model.partialorder.CRpartialorder

• • Example of a Partial Order: <CR, le>

CoRN.model.fields.Qfield

• • Example of a field: ⟨Q,+,×⟩

CoRN.model.fields.CRfield

• • Example of a field: ⟨CR,+,*⟩

CoRN.model.abgroups.QSposabgroup

• • Example of an abelian group: ⟨Q⁺, (x,y) ↦ xy/2⟩

CoRN.model.abgroups.CRabgroup

• • Example of a abelian group: ⟨CR,+⟩

CoRN.model.abgroups.Zabgroup

• • Example of an abelian group: ⟨Z,+⟩

CoRN.model.abgroups.Qposabgroup

• • Example of an abelian group: ⟨Q⁺,×⟩

CoRN.model.abgroups.Qabgroup

• • Example of an abelian group: ⟨Q,+⟩

CoRN.model.setoids.decsetoid

CoRN.model.setoids.Npossetoid

• • Example of a setoid: N⁺
    • Setoid
    • Addition and multiplication

CoRN.model.setoids.Qsetoid

• • Example of a setoid: Q
    • Setoid
    • Addition
    • Opposite
    • Multiplication
    • Less-than

CoRN.model.setoids.Nfinsetoid

• • Setoids of the first n natural numbers

CoRN.model.setoids.Zsetoid

• • Example of a setoid: Z
    • Z
    • Addition
    • Opposite
    • Multiplication
    • Zero

CoRN.model.setoids.Zfinsetoid

• • Setoids of the integers between 0 and z

CoRN.model.setoids.Nsetoid

• • Example of a setoid: N
    • Addition
    • Multiplication
    • Ternary addition

CoRN.model.setoids.Qpossetoid

• • Example of a setoid: Q⁺
    • Setoid
    • Multiplication
    • Inverse
    • Special multiplication and inverse

CoRN.model.setoids.CRsetoid

• • Example of a setoid: CR
    • CR

CoRN.model.structures.Zsec

• Z
  • About Z
    • Apartness
    • Addition
    • Multiplication
    • Miscellaneous

CoRN.model.structures.OpenUnit

• OpenUnit
  • • Equality

CoRN.model.structures.QposInf

• Q⁺

CoRN.model.structures.QnonNeg

CoRN.model.structures.NNUpperR

CoRN.model.structures.Nsec

• N
  • About N
    • Apartness
    • Addition
    • Multiplication
    • Decidability

CoRN.model.structures.Qsec

• Q
  • About Q
    • Apartness
    • Addition
    • Multiplication
    • Inverse
    • Less-than
    • Miscellaneous

CoRN.model.structures.QnnInf

CoRN.model.structures.StepQsec

• • A Partial Order on Step Functions.

CoRN.model.structures.Qinf

CoRN.model.structures.Npossec

• • N⁺

CoRN.model.structures.Qpossec

• Q⁺
  • • Equality
    • Addition
    • One
    • Multiplication
    • Inverse
    • Tactics
    • Power
    • Summing lists

CoRN.metrics.CPseudoMSpaces

• Metric Spaces (traditional)
  • Relations necessary for Pseudo Metric Spaces and Metric Spaces
  • Definition of Pseudo Metric Space
  • Pseudo Metric Space axioms
  • Pseudo Metric Space basics
  • Zero function

CoRN.metrics.LipExt

CoRN.metrics.Equiv

• • Equivalent Pseudo Metric Spaces

CoRN.metrics.IR_CPMSpace

• • Real numbers
  • Addition of continuous functions

CoRN.metrics.Prod_Sub

• • Product-Pseudo-Metric-Spaces
  • Sub-Pseudo-Metric-Spaces

CoRN.metrics.CMetricSpaces

• • Definition of Metric Space
  • Metric Space basics
  • Product-Metric-Spaces and Sub-Metric-Spaces
  • Pseudo Metric Spaces vs Metric Spaces
  • Limit

CoRN.metrics.ContFunctions

• • Continuous functions, uniformly continuous functions and Lipschitz functions
  • Identity
  • Constant functions
  • Composition
  • Limit

CoRN.metrics.CPMSTheory

• • Lists
  • Pseudo Metric Space theory

CoRN.logic.CLogic

• Extending the Coq Logic
  • Basics
  • CProp-valued Relations
  • Prop-valued Relations
  • The relation le, lt, odd and even in CProp
  • Miscellaneous
  • Results about the natural numbers
  • Algebraic Properties
  • Logical Properties
  • Integers

CoRN.logic.Classic

• Classical Logic
  • Classical or
  • Classical Existential
  • Pidgeon Hole Principle

CoRN.logic.CornBasics

• Basics
  • Some results about Z

CoRN.logic.PropDecid

• • Decidability of connectives

CoRN.logic.Stability

CoRN.ftc.FunctSequence

• Sequences of Functions
  • Definitions
  • Irrelevance of Proofs
  • Other Properties
  • Algebraic Properties

CoRN.ftc.MoreIntervals

• Generalized Intervals
  • Definitions and Basic Results
  • Constructions with Compact Intervals
  • Properties of Functions in Intervals

CoRN.ftc.RefSeparating

CoRN.ftc.Rolle

• Rolle's Theorem

CoRN.ftc.StrongIVT

• • Strong IVT for partial functions
  • Other formulations

CoRN.ftc.WeakIVT

• IVT for Partial Functions
  • First Lemmas
  • The IVT

CoRN.ftc.TaylorLemma

• Taylor's Theorem
  • First case

CoRN.ftc.RefSeparated

CoRN.ftc.IntervalFunct

• Functions with compact domain

CoRN.ftc.PartInterval

• Correspondence
  • Mappings
  • Mappings Preserve Operations

CoRN.ftc.IntegrationRules

• • Integration by substitution

CoRN.ftc.MoreFunctions

• More about Functions
  • Continuity
  • Derivative
  • Differentiability
  • Nth Derivative

CoRN.ftc.Partitions

• Partitions
  • Definitions
  • Constructions
  • Properties of the mesh
  • Miscellaneous
  • Separation

CoRN.ftc.COrdLemmas

• Lemmas for Integration
  • Merging orders
  • Summations

CoRN.ftc.MoreIntegrals

• The generalized integral
  • Definitions
  • Properties of the Integral

CoRN.ftc.MoreFunSeries

• More on Sequences and Series
  • Sequences
    • Definitions
    • Basic Properties
    • Algebraic Properties
    • Miscellaneous
  • Series
  • Algebraic Operations
    • Convergence Criteria
    • Translation

CoRN.ftc.CalculusTheorems

• Calculus Theorems

CoRN.ftc.DerivativeOps

• • Algebraic Operations
  • Local Results

CoRN.ftc.Derivative

• Derivatives
  • Basic Properties

CoRN.ftc.FunctSeries

• Series of Functions
  • Definitions
  • Convergence Criteria

CoRN.ftc.Continuity

• Continuity
  • Definitions and Basic Results
  • Algebraic Properties

CoRN.ftc.Differentiability

• Differentiability

CoRN.ftc.PartFunEquality

• Equality of Partial Functions
  • Definitions
  • Properties of Inclusion
  • Away from Zero
  • The FEQ tactic
  • Properties of Equality
  • Nth Power

CoRN.ftc.NthDerivative

• Nth Derivative
  • Definitions
  • Trivia
  • Basic Results
  • The Nth Derivative

CoRN.ftc.RefLemma

• The Refinement Lemmas

CoRN.ftc.FunctSums

• Sums of Functions

CoRN.ftc.FTC

• The Fundamental Theorem of Calculus
  • Indefinite Integrals
  • The FTC
  • Corollaries

CoRN.ftc.Composition

• Composition
  • Maps into Compacts
  • Continuity
  • Derivative
  • Differentiability
  • Generalizations

CoRN.ftc.Integral

• Integral

CoRN.ftc.RefSepRef

CoRN.ftc.Taylor

• • General case

CoRN.fta.FTAreg

• FTA for regular polynomials
  • The Kneser sequence
  • Main results
  • The Kneser sequence is Cauchy in C

CoRN.fta.KeyLemma

• Technical lemmas for the FTA
  • Key Lemma

CoRN.fta.MainLemma

• • Main Lemma

CoRN.fta.CPoly_Shift

• Shifting polynomials

CoRN.fta.KneserLemma

• • Kneser Lemma

CoRN.fta.CC_Props

• More properties of complex numbers
  • Sequences and limits
  • Continuity for C

CoRN.fta.FTA

• Fundamental Theorem of Algebra

CoRN.fta.CPoly_Contin1

• Continuity of complex polynomials

CoRN.fta.CPoly_Rev

• Reverse of polynomials

CoRN.coq_reals.Rreals

• Coq Real Numbers
  • Coq real numbers form a setoid
  • Coq real numbers form a semigroup
  • Coq real numbers form a monoid
  • Coq real numbers form a group
  • Coq real numbers form an abelian group
  • Coq real numbers form a ring
  • Coq real numbers form a field
  • Coq real numbers form an ordered field
  • Coq real numbers form a real number structure

CoRN.coq_reals.Rsign

CoRN.coq_reals.Rreals_iso

• Coq Real Numbers and IR isomorphisms
  • The isomorphism

CoRN.complex.Complex_Exponential

• • The Complex Exponential

CoRN.complex.AbsCC

• Absolute value on C
  • Properties of AbsCC
  • The triangle inequality

CoRN.complex.CComplex

• Complex Numbers
  • Algebraic structure
  • Properties of i
  • Properties of ℜ and ℑ
  • Properties of conjugation
  • Properties of the real axis
  • C has characteristic zero

CoRN.complex.NRootCC

• Roots of Complex Numbers
  • Roots of the imaginary unit
  • Roots of complex numbers

CoRN.algebra.COrdFields

• Ordered Fields
  • Definition of the notion of ordered field
  • Ordered field axioms
  • Basics
  • Basic properties of ≤
  • Infinity of ordered fields
    • Properties of one up to four
    • Properties of some other numbers
    • Consequences of infinity
  • Properties of <
    • Addition and subtraction
    • Multiplication and division
    • Miscellaneous properties

CoRN.algebra.DivDiff_RepeatedIntegral

CoRN.algebra.CornScope

CoRN.algebra.CSetoidFun

• • The Setoid of Setoid functions
  • Nullary and n-ary operations
  • Composition of Setoid functions
    • Composition as operation
    • Projections
  • Combining operations
  • The Free Setoid
  • Partial Functions
    • Subsets of Setoids
    • Operations
  • Bijections

CoRN.algebra.COrdAbs

• • Properties of AbsSmall
  • Properties of AbsBig

CoRN.algebra.OperationClasses

CoRN.algebra.CSemiGroups

• Semigroups
  • Definition of the notion of semigroup
  • Semigroup axioms
  • Semigroup basics
  • Morphism
  • About the unit
  • Functional operations
  • Subsemigroups
  • Direct Product
  • The SemiGroup of Setoid functions
  • The Free SemiGroup

CoRN.algebra.CRing_Homomorphisms

• Ring Homomorphisms
  • Definition of Ring Homomorphisms
  • Lemmas on Ring Homomorphisms
    • Axioms on Ring Homomorphisms
    • Facts on Ring Homomorphisms

CoRN.algebra.CPoly_Lagrange

CoRN.algebra.RSetoid

• Classic Setoids presented in a bundled way.
• THIS NOTION IS OBSOLETE AND SHOULD NOT BE USED ANYMORE
• Use abstract_algebra.Setoid instead
  • Morhpisms between Setoids
  • Basic Combinators for Setoids

CoRN.algebra.CPoly_Newton

CoRN.algebra.CSetoids

• Setoids
  • Relations necessary for Setoids
  • Definition of Setoid
  • Setoid axioms
  • Setoid basics
  • The product of setoids
  • Relations and predicates
    • Predicates
    • Definition of a setoid predicate
    • Relations
    • Definition of a setoid relation
    • CProp Relations
    • Definition of a CProp setoid relation
  • Functions between setoids
  • The unary and binary (inner) operations on a csetoid
  • The binary outer operations on a csetoid
  • Subsetoids
    • Subsetoid unary operations
    • Subsetoid binary operations
  • Miscellaneous

CoRN.algebra.CPoly_NthCoeff

• Polynomials: Nth Coefficient
  • Definitions
  • Properties of nth_coeff

CoRN.algebra.CPoly_ApZero

• Polynomials apart from zero
  • Representation of polynomials
  • Polynomials are nonzero on any interval

CoRN.algebra.CFields

• Fields
  • Definition of the notion Field
  • Field axioms
  • Field basics
  • Properties of multiplication
  • Properties of reciprocal
  • The multiplicative group of nonzeros of a field.
  • Properties of division
  • Cancellation laws for apartness and multiplication
  • Functional Operations

CoRN.algebra.COrdFields2

• • Properties of ≤
    • Addition and subtraction
    • Multiplication and division
    • Miscellaneous Properties
  • Properties of positive numbers
  • Properties of one over successor
  • Properties of ½

CoRN.algebra.CMonoids

• Monoids
  • Definition of monoids
  • Monoid axioms
  • Monoid basics
  • Submonoids
  • Morphism, isomorphism and automorphism of Monoids
  • Power in a monoid
  • Cyclicity
  • Invertability
  • Direct Product
  • The Monoids of Setoid functions and bijective Setoid functions.
  • The free Monoid
  • The unit in the setoid of Setoid functions
  • Intersection

CoRN.algebra.CAbMonoids

• Abelian Monoids
  • Subgroups of an Abelian Monoid

CoRN.algebra.COrdCauchy

• • Cauchy sequences
  • Multiplication is continuous
  • Monotonous Functions

CoRN.algebra.CAbGroups

• Abelian Groups
  • Subgroups of an Abelian Group
  • Basic properties of Abelian groups
  • Building an abelian group
  • Iteration

CoRN.algebra.CRingClass

CoRN.algebra.RingClass

CoRN.algebra.CPolynomials

• Polynomials
  • Definition of polynomials; they form a ring
    • The polynomials form a setoid
    • The polynomials form a semi-group and a monoid
    • The polynomials form a group
    • The polynomials form a ring
  • Apartness, equality, and induction
  • Basic properties of polynomials
    • Constant and identity
    • Application of polynomials
  • Induction properties of polynomials for Prop

CoRN.algebra.CPoly_Euclid

CoRN.algebra.CPoly_Degree

• Degrees of Polynomials
  • Degrees of polynomials over a ring
  • Degrees of polynomials over a field

CoRN.algebra.CGroups

• Groups
  • Definition of the notion of Group
  • Group axioms
  • Group basics
  • Sub-groups
  • Associative properties of groups
  • Apartness in Constructive Groups
  • The Group of bijective Setoid functions
  • Functional operations

CoRN.algebra.Expon

• Exponentiation
  • More properties about nexp
  • Definition of zexp: integer exponentiation
  • Properties of zexp

CoRN.algebra.CSums

• Sums

CoRN.algebra.Ranges

CoRN.algebra.CRing_as_Ring

CoRN.algebra.CSetoidInc

• • Inclusion

CoRN.algebra.Bernstein

• • Bernstein Polynomials

CoRN.algebra.CRings

• Rings
  • Definition of the notion of Ring
  • Ring axioms
  • Ring constructions
  • Ring unfolded
  • Ring basics
  • Ring Definitions
    • Exponentiation
    • The injection of natural numbers into a ring
    • The injection of integers into a ring
  • Ring sums
    • Infinite Ring sums
    • Ring Sums over Lists
  • Distribution properties
  • Properties of exponentiation (with the exponent in N)
  • Functional Operations

CoRN.algebra.Cauchy_COF

• The Field of Cauchy Sequences
  • Setoid Structure
  • Group Structure
  • Ring Structure
  • Field Structure
  • Order Structure
  • Other Results

CoRN.MathClasses.categories.cat

CoRN.MathClasses.categories.JMcat

CoRN.MathClasses.categories.unit

CoRN.MathClasses.categories.algebra

CoRN.MathClasses.categories.setoid

CoRN.MathClasses.categories.dual

CoRN.MathClasses.categories.variety

CoRN.MathClasses.categories.product

CoRN.MathClasses.categories.empty

CoRN.MathClasses.categories.functor

CoRN.MathClasses.misc.setoid_tactics

CoRN.MathClasses.misc.workarounds

CoRN.MathClasses.misc.JMrelation

CoRN.MathClasses.misc.util

CoRN.MathClasses.misc.workaround_tactics

CoRN.MathClasses.theory.monads

CoRN.MathClasses.theory.forget_variety

CoRN.MathClasses.theory.series

CoRN.MathClasses.theory.ua_products

CoRN.MathClasses.theory.nat_pow

CoRN.MathClasses.theory.strong_setoids

CoRN.MathClasses.theory.cut_minus

CoRN.MathClasses.theory.hom_functor

CoRN.MathClasses.theory.ua_transference

CoRN.MathClasses.theory.sequences

CoRN.MathClasses.theory.functors

CoRN.MathClasses.theory.ua_term_monad

CoRN.MathClasses.theory.groups

CoRN.MathClasses.theory.dec_fields

CoRN.MathClasses.theory.ua_mapped_operations

CoRN.MathClasses.theory.categories

CoRN.MathClasses.theory.nat_distance

CoRN.MathClasses.theory.ua_packed

CoRN.MathClasses.theory.ua_subvariety

CoRN.MathClasses.theory.int_pow

CoRN.MathClasses.theory.abs

CoRN.MathClasses.theory.shiftl

CoRN.MathClasses.theory.ring_ideals

CoRN.MathClasses.theory.adjunctions

CoRN.MathClasses.theory.fields

CoRN.MathClasses.theory.naturals

CoRN.MathClasses.theory.forget_algebra

CoRN.MathClasses.theory.ua_subalgebra

CoRN.MathClasses.theory.ua_subalgebraT

CoRN.MathClasses.theory.setoids

CoRN.MathClasses.theory.ua_homomorphisms

CoRN.MathClasses.theory.streams

CoRN.MathClasses.theory.rationals

CoRN.MathClasses.theory.integers

CoRN.MathClasses.theory.int_abs

CoRN.MathClasses.theory.jections

CoRN.MathClasses.theory.rings

CoRN.MathClasses.theory.monoid_normalization

CoRN.MathClasses.theory.ua_congruence

CoRN.MathClasses.theory.quote_monoid

CoRN.MathClasses.interfaces.monads

CoRN.MathClasses.interfaces.sequences

CoRN.MathClasses.interfaces.functors

CoRN.MathClasses.interfaces.additional_operations

CoRN.MathClasses.interfaces.orders

CoRN.MathClasses.interfaces.canonical_names

CoRN.MathClasses.interfaces.ua_basic

CoRN.MathClasses.interfaces.vectorspace

CoRN.MathClasses.interfaces.abstract_algebra

CoRN.MathClasses.interfaces.naturals

CoRN.MathClasses.interfaces.rationals

CoRN.MathClasses.interfaces.integers

CoRN.MathClasses.interfaces.universal_algebra

CoRN.MathClasses.implementations.fast_rationals

CoRN.MathClasses.implementations.polynomials

CoRN.MathClasses.implementations.positive_semiring_elements

CoRN.MathClasses.implementations.stdlib_binary_naturals

CoRN.MathClasses.implementations.fast_naturals

CoRN.MathClasses.implementations.nonzero_field_elements

CoRN.MathClasses.implementations.natpair_integers

CoRN.MathClasses.implementations.fast_integers

CoRN.MathClasses.implementations.semiring_pairs

CoRN.MathClasses.implementations.NType_naturals

CoRN.MathClasses.implementations.nonneg_integers_naturals

CoRN.MathClasses.implementations.ne_list

CoRN.MathClasses.implementations.dyadics

CoRN.MathClasses.implementations.stdlib_rationals

CoRN.MathClasses.implementations.nonneg_semiring_elements

CoRN.MathClasses.implementations.cons_list

CoRN.MathClasses.implementations.intfrac_rationals

CoRN.MathClasses.implementations.stdlib_binary_integers

CoRN.MathClasses.implementations.peano_naturals

CoRN.MathClasses.implementations.QType_rationals

CoRN.MathClasses.implementations.field_of_fractions

CoRN.MathClasses.implementations.ZType_integers

CoRN.MathClasses.varieties.open_terms

CoRN.MathClasses.varieties.semiring

CoRN.MathClasses.varieties.closed_terms

CoRN.MathClasses.varieties.setoid

CoRN.MathClasses.varieties.group

CoRN.MathClasses.varieties.monoid

CoRN.MathClasses.varieties.empty

CoRN.MathClasses.varieties.ring

CoRN.MathClasses.varieties.semigroup

CoRN.MathClasses.quote.classquote

CoRN.MathClasses.orders.semirings

CoRN.MathClasses.orders.dec_fields

CoRN.MathClasses.orders.orders

CoRN.MathClasses.orders.minmax

CoRN.MathClasses.orders.naturals

CoRN.MathClasses.orders.maps

CoRN.MathClasses.orders.rationals

CoRN.MathClasses.orders.integers

CoRN.MathClasses.orders.rings