Code

WIP: eudoxus reals#116

Code

Draft

strub wants to merge 17 commits intomastermath-comp/analysis:masterfrom eudoxus-realsmath-comp/analysis:eudoxus-realsCopy head branch name to clipboard

+1,222

Commits

Commits on Oct 17, 2018

• WIP: eudoxus reals

  strub

  committed
  b4f975c

  Copy full SHA for b4f975c

• Def. of the eudoxus reals + zmod structure + mul def + basic properties on mul

  strub

  committed
  6eabce0

  Copy full SHA for 6eabce0

Commits on Oct 18, 2018

• Eudoxus reals: ring structure + refactoring

  strub

  committed
  a1a5f58

  Copy full SHA for a1a5f58

• _CoqProject

  strub

  committed
  c184a93

  Copy full SHA for c184a93

• NumMixin from a "being positive" predicate

  strub

  committed
  5e0684f

  Copy full SHA for 5e0684f

Commits on Oct 23, 2018

• core lemma for eudoxus reals classification wrt 0

  strub

  committed
  f61be66

  Copy full SHA for f61be66

• Completed proof that eudoxus reals form an ordered num domain

  strub

  committed
  57da9d7

  Copy full SHA for 57da9d7

Commits on Oct 25, 2018

• eudoxus reals: prove the Archimedean property

  strub

  committed
  956ed96

  Copy full SHA for 956ed96

• nits

  strub

  committed
  d85ff0d

  Copy full SHA for d85ff0d

• qzendo from qzendo on nat

  strub

  committed
  96c6640

  Copy full SHA for 96c6640

Commits on Oct 25, 2019

• Merge branch 'master' into eudoxus-reals

  strub

  committed
  604f8e1

  Copy full SHA for 604f8e1

• Draft

  strub

  committed
  a999302

  Copy full SHA for a999302

Commits on Jan 24, 2020

• Merge remote-tracking branch 'origin/master' into eudoxus-reals

  strub

  committed
  f2bc260

  Copy full SHA for f2bc260

Commits on Nov 6, 2020

• strub

  committed
  9d20d85

  Copy full SHA for 9d20d85

• Merge remote-tracking branch 'origin/master' into eudoxus-reals

  strub

  committed
  d86c872

  Copy full SHA for d86c872

• make things compiling again

  strub

  committed
  de2a47b

  Copy full SHA for de2a47b

Commits on Jun 9, 2021

• Merge branch 'master' into eudoxus-reals

  strub

  committed
  3404e59

  Copy full SHA for 3404e59