Code

Negation on real numbers#1246

Code

Open

lowasser wants to merge 21 commits intoUniMath:masterUniMath/agda-unimath:masterfrom lowasser:negate-reallowasser/agda-unimath:negate-realCopy head branch name to clipboard

+190

Commits

Commits on Jan 20, 2025

• Define the theorem to prove

  lowasser

  committed
  c50af11

  Copy full SHA for c50af11

• Define the theorem on integer fractions

  lowasser

  committed
  8384f31

  Copy full SHA for 8384f31

• Prove the theorem on integers

  lowasser

  committed
  fd7c613

  Copy full SHA for fd7c613

Commits on Jan 21, 2025

• Prove the theorem on rationals

  lowasser

  committed
  e0ed494

  Copy full SHA for e0ed494

Commits on Jan 29, 2025

• Add lowasser to CONTRIBUTORS.toml

  lowasser

  committed
  d3cea33

  Copy full SHA for d3cea33

• Define the negation of a real number, and prove it is itself real.

  lowasser

  committed
  e292096

  Copy full SHA for e292096

• Make naming slightly more consistent with precedent.

  lowasser

  committed
  beeb272

  Copy full SHA for beeb272

• Merge branch 'add-contributor' into negate-real

  lowasser

  committed
  ab72c9c

  Copy full SHA for ab72c9c

Commits on Jan 30, 2025

• Typo fix

  lowasser

  committed
  a40d503

  Copy full SHA for a40d503

• Fix file header

  lowasser

  committed
  1f46e1a

  Copy full SHA for 1f46e1a

Commits on Jan 31, 2025

• make pre-commit updates

  lowasser

  committed
  7b32078

  Copy full SHA for 7b32078

• Merge branch 'master' into negation-rational-ordering

  lowasser

  committed
  cb88d47

  Copy full SHA for cb88d47

• Fix indentation style

  lowasser

  committed
  c1092af

  Copy full SHA for c1092af

• Fix more indentatino

  lowasser

  committed
  4158618

  Copy full SHA for 4158618

• Merge branch 'negation-rational-ordering' into negate-real

  lowasser

  committed
  825a6eb

  Copy full SHA for 825a6eb

• Attempt to fix indentation

  lowasser

  committed
  201c3a4

  Copy full SHA for 201c3a4

• Merge branch 'master' into negate-real

  lowasser

  authored
  8024abd

  Copy full SHA for 8024abd

• Fix missed indentation

  lowasser

  committed
  e4a16c9

  Copy full SHA for e4a16c9

• Merge remote-tracking branch 'origin/negate-real' into negate-real

  lowasser

  committed
  fed17cd

  Copy full SHA for fed17cd

• Merge branch 'master' into negate-real

  lowasser

  authored
  26bf7ec

  Copy full SHA for 26bf7ec

Commits on Feb 1, 2025

• Apply suggestions from code review

  Show description for 2ab1490
  

  3 peopleauthored
  2ab1490

  Copy full SHA for 2ab1490