From 1b013938608531843296f4bc736e0f846193c370 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 9 Apr 2024 21:04:29 +0200 Subject: [PATCH] The additive group of rational numbers (#1100) This pull requests introduces the additive group structure on the rational numbers. We introduce - the `neg-fraction-Z` and `neg-Q` functions and some basic properties with respect to addition and multiplication. - the difference of rational numbers and some basic properties with respect to addition and multiplication. We also prove associativity and commutativity of multiplication on the rational numbers. --------- Co-authored-by: Fredrik Bakke --- ...les-of-elements-commutative-rings.lagda.md | 4 +- src/elementary-number-theory.lagda.md | 2 + .../addition-integer-fractions.lagda.md | 271 +++++++++------ .../addition-integers.lagda.md | 329 +++++++++--------- .../addition-natural-numbers.lagda.md | 166 +++++---- ...on-positive-and-negative-integers.lagda.md | 146 ++++---- .../addition-rational-numbers.lagda.md | 154 +++++--- .../bezouts-lemma-integers.lagda.md | 4 +- ...tion-difference-integer-fractions.lagda.md | 6 +- .../difference-integers.lagda.md | 220 +++++++----- .../difference-rational-numbers.lagda.md | 154 ++++++++ .../greatest-common-divisor-integers.lagda.md | 16 + .../group-of-rational-numbers.lagda.md | 55 +++ .../inequality-integer-fractions.lagda.md | 2 +- .../inequality-integers.lagda.md | 73 ++++ .../inequality-rational-numbers.lagda.md | 4 +- .../integer-fractions.lagda.md | 191 ++++++---- .../integers.lagda.md | 99 +++--- .../modular-arithmetic.lagda.md | 6 +- .../multiplication-integer-fractions.lagda.md | 8 +- .../multiplication-integers.lagda.md | 144 +++++--- ...on-positive-and-negative-integers.lagda.md | 20 +- .../multiplication-rational-numbers.lagda.md | 129 ++++++- .../negative-integers.lagda.md | 8 + .../nonzero-integers.lagda.md | 7 + .../positive-and-negative-integers.lagda.md | 15 +- .../positive-integers.lagda.md | 8 + .../rational-numbers.lagda.md | 148 ++++++-- .../reduced-integer-fractions.lagda.md | 16 + .../ring-of-integers.lagda.md | 11 +- ...rict-inequality-integer-fractions.lagda.md | 14 + .../strict-inequality-integers.lagda.md | 71 ++++ ...trict-inequality-rational-numbers.lagda.md | 49 ++- ...tiples-of-elements-abelian-groups.lagda.md | 4 +- ...integer-powers-of-elements-groups.lagda.md | 38 +- .../rational-real-numbers.lagda.md | 34 +- ...teger-multiples-of-elements-rings.lagda.md | 4 +- 37 files changed, 1788 insertions(+), 842 deletions(-) create mode 100644 src/elementary-number-theory/difference-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/group-of-rational-numbers.lagda.md diff --git a/src/commutative-algebra/integer-multiples-of-elements-commutative-rings.lagda.md b/src/commutative-algebra/integer-multiples-of-elements-commutative-rings.lagda.md index 412b24456b..ea8f228c18 100644 --- a/src/commutative-algebra/integer-multiples-of-elements-commutative-rings.lagda.md +++ b/src/commutative-algebra/integer-multiples-of-elements-commutative-rings.lagda.md @@ -99,14 +99,14 @@ module _ integer-multiple-in-pos-Commutative-Ring : (n : ℕ) (a : type-Commutative-Ring A) → - integer-multiple-Commutative-Ring A (in-pos n) a ＝ + integer-multiple-Commutative-Ring A (in-pos-ℤ n) a ＝ multiple-Commutative-Ring A (succ-ℕ n) a integer-multiple-in-pos-Commutative-Ring = integer-multiple-in-pos-Ring (ring-Commutative-Ring A) integer-multiple-in-neg-Commutative-Ring : (n : ℕ) (a : type-Commutative-Ring A) → - integer-multiple-Commutative-Ring A (in-neg n) a ＝ + integer-multiple-Commutative-Ring A (in-neg-ℤ n) a ＝ neg-Commutative-Ring A (multiple-Commutative-Ring A (succ-ℕ n) a) integer-multiple-in-neg-Commutative-Ring = integer-multiple-in-neg-Ring (ring-Commutative-Ring A) diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index dbf5dd22d6..58a4cc7ffa 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -37,6 +37,7 @@ open import elementary-number-theory.decidable-total-order-rational-numbers publ open import elementary-number-theory.decidable-total-order-standard-finite-types public open import elementary-number-theory.decidable-types public open import elementary-number-theory.difference-integers public +open import elementary-number-theory.difference-rational-numbers public open import elementary-number-theory.dirichlet-convolution public open import elementary-number-theory.distance-integers public open import elementary-number-theory.distance-natural-numbers public @@ -59,6 +60,7 @@ open import elementary-number-theory.goldbach-conjecture public open import elementary-number-theory.greatest-common-divisor-integers public open import elementary-number-theory.greatest-common-divisor-natural-numbers public open import elementary-number-theory.group-of-integers public +open import elementary-number-theory.group-of-rational-numbers public open import elementary-number-theory.half-integers public open import elementary-number-theory.hardy-ramanujan-number public open import elementary-number-theory.inequality-integer-fractions public diff --git a/src/elementary-number-theory/addition-integer-fractions.lagda.md b/src/elementary-number-theory/addition-integer-fractions.lagda.md index adfbc5841a..6b438b35c9 100644 --- a/src/elementary-number-theory/addition-integer-fractions.lagda.md +++ b/src/elementary-number-theory/addition-integer-fractions.lagda.md @@ -9,10 +9,12 @@ module elementary-number-theory.addition-integer-fractions where ```agda open import elementary-number-theory.addition-integers open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-positive-and-negative-integers open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types ``` @@ -52,134 +54,175 @@ ap-add-fraction-ℤ p q = ap-binary add-fraction-ℤ p q ### Addition respects the similarity relation ```agda -sim-fraction-add-fraction-ℤ : - {x x' y y' : fraction-ℤ} → - sim-fraction-ℤ x x' → - sim-fraction-ℤ y y' → - sim-fraction-ℤ (x +fraction-ℤ y) (x' +fraction-ℤ y') -sim-fraction-add-fraction-ℤ - {(nx , dx , dxp)} {(nx' , dx' , dx'p)} - {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q = - equational-reasoning - ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ (dx' *ℤ dy') - ＝ ((nx *ℤ dy) *ℤ (dx' *ℤ dy')) +ℤ ((ny *ℤ dx) *ℤ (dx' *ℤ dy')) - by right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) (dx' *ℤ dy') - ＝ ((dy *ℤ nx) *ℤ (dx' *ℤ dy')) +ℤ ((dx *ℤ ny) *ℤ (dy' *ℤ dx')) - by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ nx dy) refl) - (ap-mul-ℤ (commutative-mul-ℤ ny dx) (commutative-mul-ℤ dx' dy')) - ＝ (((dy *ℤ nx) *ℤ dx') *ℤ dy') +ℤ (((dx *ℤ ny) *ℤ dy') *ℤ dx') - by ap-add-ℤ (inv (associative-mul-ℤ (dy *ℤ nx) dx' dy')) - (inv (associative-mul-ℤ (dx *ℤ ny) dy' dx')) - ＝ ((dy *ℤ (nx *ℤ dx')) *ℤ dy') +ℤ ((dx *ℤ (ny *ℤ dy')) *ℤ dx') - by ap-add-ℤ (ap-mul-ℤ (associative-mul-ℤ dy nx dx') refl) - (ap-mul-ℤ (associative-mul-ℤ dx ny dy') refl) - ＝ ((dy *ℤ (dx *ℤ nx')) *ℤ dy') +ℤ ((dx *ℤ (dy *ℤ ny')) *ℤ dx') - by ap-add-ℤ - (ap-mul-ℤ (ap-mul-ℤ (refl {x = dy}) (p ∙ commutative-mul-ℤ nx' dx)) - (refl {x = dy'})) - (ap-mul-ℤ (ap-mul-ℤ (refl {x = dx}) (q ∙ commutative-mul-ℤ ny' dy)) - (refl {x = dx'})) - ＝ (((dy *ℤ dx) *ℤ nx') *ℤ dy') +ℤ (((dx *ℤ dy) *ℤ ny') *ℤ dx') - by ap-add-ℤ (ap-mul-ℤ (inv (associative-mul-ℤ dy dx nx')) refl) - (ap-mul-ℤ (inv (associative-mul-ℤ dx dy ny')) refl) - ＝ ((nx' *ℤ (dy *ℤ dx)) *ℤ dy') +ℤ ((ny' *ℤ (dx *ℤ dy)) *ℤ dx') - by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ (dy *ℤ dx) nx') refl) - (ap-mul-ℤ (commutative-mul-ℤ (dx *ℤ dy) ny') refl) - ＝ (nx' *ℤ ((dy *ℤ dx) *ℤ dy')) +ℤ (ny' *ℤ ((dx *ℤ dy) *ℤ dx')) - by ap-add-ℤ (associative-mul-ℤ nx' (dy *ℤ dx) dy') - (associative-mul-ℤ ny' (dx *ℤ dy) dx') - ＝ (nx' *ℤ (dy' *ℤ (dy *ℤ dx))) +ℤ (ny' *ℤ (dx' *ℤ (dx *ℤ dy))) - by ap-add-ℤ - (ap-mul-ℤ (refl {x = nx'}) (commutative-mul-ℤ (dy *ℤ dx) dy')) - (ap-mul-ℤ (refl {x = ny'}) (commutative-mul-ℤ (dx *ℤ dy) dx')) - ＝ ((nx' *ℤ dy') *ℤ (dy *ℤ dx)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) - by ap-add-ℤ (inv (associative-mul-ℤ nx' dy' (dy *ℤ dx))) - (inv (associative-mul-ℤ ny' dx' (dx *ℤ dy))) - ＝ ((nx' *ℤ dy') *ℤ (dx *ℤ dy)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) - by ap-add-ℤ - (ap-mul-ℤ (refl {x = nx' *ℤ dy'}) (commutative-mul-ℤ dy dx)) refl - ＝ ((nx' *ℤ dy') +ℤ (ny' *ℤ dx')) *ℤ (dx *ℤ dy) - by inv (right-distributive-mul-add-ℤ (nx' *ℤ dy') _ (dx *ℤ dy)) +abstract + sim-fraction-add-fraction-ℤ : + {x x' y y' : fraction-ℤ} → + sim-fraction-ℤ x x' → + sim-fraction-ℤ y y' → + sim-fraction-ℤ (x +fraction-ℤ y) (x' +fraction-ℤ y') + sim-fraction-add-fraction-ℤ + {(nx , dx , dxp)} {(nx' , dx' , dx'p)} + {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q = + equational-reasoning + ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ (dx' *ℤ dy') + ＝ ((nx *ℤ dy) *ℤ (dx' *ℤ dy')) +ℤ ((ny *ℤ dx) *ℤ (dx' *ℤ dy')) + by right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) (dx' *ℤ dy') + ＝ ((dy *ℤ nx) *ℤ (dx' *ℤ dy')) +ℤ ((dx *ℤ ny) *ℤ (dy' *ℤ dx')) + by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ nx dy) refl) + (ap-mul-ℤ (commutative-mul-ℤ ny dx) (commutative-mul-ℤ dx' dy')) + ＝ (((dy *ℤ nx) *ℤ dx') *ℤ dy') +ℤ (((dx *ℤ ny) *ℤ dy') *ℤ dx') + by ap-add-ℤ (inv (associative-mul-ℤ (dy *ℤ nx) dx' dy')) + (inv (associative-mul-ℤ (dx *ℤ ny) dy' dx')) + ＝ ((dy *ℤ (nx *ℤ dx')) *ℤ dy') +ℤ ((dx *ℤ (ny *ℤ dy')) *ℤ dx') + by ap-add-ℤ (ap-mul-ℤ (associative-mul-ℤ dy nx dx') refl) + (ap-mul-ℤ (associative-mul-ℤ dx ny dy') refl) + ＝ ((dy *ℤ (dx *ℤ nx')) *ℤ dy') +ℤ ((dx *ℤ (dy *ℤ ny')) *ℤ dx') + by ap-add-ℤ + (ap-mul-ℤ (ap-mul-ℤ (refl {x = dy}) (p ∙ commutative-mul-ℤ nx' dx)) + (refl {x = dy'})) + (ap-mul-ℤ (ap-mul-ℤ (refl {x = dx}) (q ∙ commutative-mul-ℤ ny' dy)) + (refl {x = dx'})) + ＝ (((dy *ℤ dx) *ℤ nx') *ℤ dy') +ℤ (((dx *ℤ dy) *ℤ ny') *ℤ dx') + by ap-add-ℤ (ap-mul-ℤ (inv (associative-mul-ℤ dy dx nx')) refl) + (ap-mul-ℤ (inv (associative-mul-ℤ dx dy ny')) refl) + ＝ ((nx' *ℤ (dy *ℤ dx)) *ℤ dy') +ℤ ((ny' *ℤ (dx *ℤ dy)) *ℤ dx') + by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ (dy *ℤ dx) nx') refl) + (ap-mul-ℤ (commutative-mul-ℤ (dx *ℤ dy) ny') refl) + ＝ (nx' *ℤ ((dy *ℤ dx) *ℤ dy')) +ℤ (ny' *ℤ ((dx *ℤ dy) *ℤ dx')) + by ap-add-ℤ (associative-mul-ℤ nx' (dy *ℤ dx) dy') + (associative-mul-ℤ ny' (dx *ℤ dy) dx') + ＝ (nx' *ℤ (dy' *ℤ (dy *ℤ dx))) +ℤ (ny' *ℤ (dx' *ℤ (dx *ℤ dy))) + by ap-add-ℤ + (ap-mul-ℤ (refl {x = nx'}) (commutative-mul-ℤ (dy *ℤ dx) dy')) + (ap-mul-ℤ (refl {x = ny'}) (commutative-mul-ℤ (dx *ℤ dy) dx')) + ＝ ((nx' *ℤ dy') *ℤ (dy *ℤ dx)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) + by ap-add-ℤ (inv (associative-mul-ℤ nx' dy' (dy *ℤ dx))) + (inv (associative-mul-ℤ ny' dx' (dx *ℤ dy))) + ＝ ((nx' *ℤ dy') *ℤ (dx *ℤ dy)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) + by ap-add-ℤ + (ap-mul-ℤ (refl {x = nx' *ℤ dy'}) (commutative-mul-ℤ dy dx)) refl + ＝ ((nx' *ℤ dy') +ℤ (ny' *ℤ dx')) *ℤ (dx *ℤ dy) + by inv (right-distributive-mul-add-ℤ (nx' *ℤ dy') _ (dx *ℤ dy)) ``` ### Unit laws ```agda -left-unit-law-add-fraction-ℤ : - (k : fraction-ℤ) → - sim-fraction-ℤ (zero-fraction-ℤ +fraction-ℤ k) k -left-unit-law-add-fraction-ℤ (m , n , p) = - ap-mul-ℤ (right-unit-law-mul-ℤ m) refl - -right-unit-law-add-fraction-ℤ : - (k : fraction-ℤ) → - sim-fraction-ℤ (k +fraction-ℤ zero-fraction-ℤ) k -right-unit-law-add-fraction-ℤ (m , n , p) = - ap-mul-ℤ - ( ap-add-ℤ (right-unit-law-mul-ℤ m) refl ∙ right-unit-law-add-ℤ m) - ( inv (right-unit-law-mul-ℤ n)) +abstract + left-unit-law-add-fraction-ℤ : + (k : fraction-ℤ) → + sim-fraction-ℤ (zero-fraction-ℤ +fraction-ℤ k) k + left-unit-law-add-fraction-ℤ (m , n , p) = + ap-mul-ℤ (right-unit-law-mul-ℤ m) refl + + right-unit-law-add-fraction-ℤ : + (k : fraction-ℤ) → + sim-fraction-ℤ (k +fraction-ℤ zero-fraction-ℤ) k + right-unit-law-add-fraction-ℤ (m , n , p) = + ap-mul-ℤ + ( ap-add-ℤ (right-unit-law-mul-ℤ m) refl ∙ right-unit-law-add-ℤ m) + ( inv (right-unit-law-mul-ℤ n)) ``` ### Addition is associative ```agda -associative-add-fraction-ℤ : - (x y z : fraction-ℤ) → - sim-fraction-ℤ - ((x +fraction-ℤ y) +fraction-ℤ z) - (x +fraction-ℤ (y +fraction-ℤ z)) -associative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = - ap-mul-ℤ (eq-num) (inv (associative-mul-ℤ dx dy dz)) - where - eq-num : - ( ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) ＝ - ( (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx)) - eq-num = - equational-reasoning - (((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) - ＝ (((nx *ℤ dy) *ℤ dz) +ℤ ((ny *ℤ dx) *ℤ dz)) +ℤ - (nz *ℤ (dx *ℤ dy)) - by ap-add-ℤ - (right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) dz) refl - ＝ ((nx *ℤ dy) *ℤ dz) +ℤ - (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) - by associative-add-ℤ - ((nx *ℤ dy) *ℤ dz) ((ny *ℤ dx) *ℤ dz) _ - ＝ (nx *ℤ (dy *ℤ dz)) +ℤ - (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) - by ap-add-ℤ (associative-mul-ℤ nx dy dz) refl - ＝ (nx *ℤ (dy *ℤ dz)) +ℤ - ((ny *ℤ (dz *ℤ dx)) +ℤ (nz *ℤ (dy *ℤ dx))) - by ap-add-ℤ - (refl {x = nx *ℤ (dy *ℤ dz)}) - (ap-add-ℤ - (associative-mul-ℤ ny dx dz ∙ ap-mul-ℤ (refl {x = ny}) - (commutative-mul-ℤ dx dz)) - (ap-mul-ℤ (refl {x = nz}) (commutative-mul-ℤ dx dy))) - ＝ (nx *ℤ (dy *ℤ dz)) +ℤ - (((ny *ℤ dz) *ℤ dx) +ℤ ((nz *ℤ dy) *ℤ dx)) - by ap-add-ℤ - (refl {x = nx *ℤ (dy *ℤ dz)}) - (inv +abstract + associative-add-fraction-ℤ : + (x y z : fraction-ℤ) → + sim-fraction-ℤ + ((x +fraction-ℤ y) +fraction-ℤ z) + (x +fraction-ℤ (y +fraction-ℤ z)) + associative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = + ap-mul-ℤ (eq-num) (inv (associative-mul-ℤ dx dy dz)) + where + eq-num : + ( ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) ＝ + ( (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx)) + eq-num = + equational-reasoning + (((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) + ＝ (((nx *ℤ dy) *ℤ dz) +ℤ ((ny *ℤ dx) *ℤ dz)) +ℤ + (nz *ℤ (dx *ℤ dy)) + by ap-add-ℤ + (right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) dz) refl + ＝ ((nx *ℤ dy) *ℤ dz) +ℤ + (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) + by associative-add-ℤ + ((nx *ℤ dy) *ℤ dz) ((ny *ℤ dx) *ℤ dz) _ + ＝ (nx *ℤ (dy *ℤ dz)) +ℤ + (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) + by ap-add-ℤ (associative-mul-ℤ nx dy dz) refl + ＝ (nx *ℤ (dy *ℤ dz)) +ℤ + ((ny *ℤ (dz *ℤ dx)) +ℤ (nz *ℤ (dy *ℤ dx))) + by ap-add-ℤ + (refl {x = nx *ℤ (dy *ℤ dz)}) (ap-add-ℤ - ( associative-mul-ℤ ny dz dx) - ( associative-mul-ℤ nz dy dx))) - ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx) - by ap-add-ℤ - (refl {x = nx *ℤ (dy *ℤ dz)}) - (inv (right-distributive-mul-add-ℤ (ny *ℤ dz) (nz *ℤ dy) dx)) + (associative-mul-ℤ ny dx dz ∙ ap-mul-ℤ (refl {x = ny}) + (commutative-mul-ℤ dx dz)) + (ap-mul-ℤ (refl {x = nz}) (commutative-mul-ℤ dx dy))) + ＝ (nx *ℤ (dy *ℤ dz)) +ℤ + (((ny *ℤ dz) *ℤ dx) +ℤ ((nz *ℤ dy) *ℤ dx)) + by ap-add-ℤ + (refl {x = nx *ℤ (dy *ℤ dz)}) + (inv + (ap-add-ℤ + ( associative-mul-ℤ ny dz dx) + ( associative-mul-ℤ nz dy dx))) + ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx) + by ap-add-ℤ + (refl {x = nx *ℤ (dy *ℤ dz)}) + (inv (right-distributive-mul-add-ℤ (ny *ℤ dz) (nz *ℤ dy) dx)) ``` ### Addition is commutative ```agda -commutative-add-fraction-ℤ : - (x y : fraction-ℤ) → - sim-fraction-ℤ - (x +fraction-ℤ y) - (y +fraction-ℤ x) -commutative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = - ap-mul-ℤ - ( commutative-add-ℤ (nx *ℤ dy) (ny *ℤ dx)) - ( commutative-mul-ℤ dy dx) +abstract + commutative-add-fraction-ℤ : + (x y : fraction-ℤ) → + sim-fraction-ℤ + (x +fraction-ℤ y) + (y +fraction-ℤ x) + commutative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = + ap-mul-ℤ + ( commutative-add-ℤ (nx *ℤ dy) (ny *ℤ dx)) + ( commutative-mul-ℤ dy dx) +``` + +### The numerator of the sum of an integer fraction and its negative is zero + +```agda +abstract + is-zero-numerator-add-left-neg-fraction-ℤ : + (x : fraction-ℤ) → + is-zero-ℤ (numerator-fraction-ℤ (add-fraction-ℤ (neg-fraction-ℤ x) x)) + is-zero-numerator-add-left-neg-fraction-ℤ (p , q , H) = + ap (_+ℤ (p *ℤ q)) (left-negative-law-mul-ℤ p q) ∙ + left-inverse-law-add-ℤ (p *ℤ q) + + is-zero-numerator-add-right-neg-fraction-ℤ : + (x : fraction-ℤ) → + is-zero-ℤ (numerator-fraction-ℤ (add-fraction-ℤ x (neg-fraction-ℤ x))) + is-zero-numerator-add-right-neg-fraction-ℤ (p , q , H) = + ap ((p *ℤ q) +ℤ_) (left-negative-law-mul-ℤ p q) ∙ + right-inverse-law-add-ℤ (p *ℤ q) +``` + +### Distributivity of negatives over addition on the integer fractions + +```agda +abstract + distributive-neg-add-fraction-ℤ : + (x y : fraction-ℤ) → + sim-fraction-ℤ + (neg-fraction-ℤ (x +fraction-ℤ y)) + (neg-fraction-ℤ x +fraction-ℤ neg-fraction-ℤ y) + distributive-neg-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = + ap + ( _*ℤ (dx *ℤ dy)) + ( ( distributive-neg-add-ℤ (nx *ℤ dy) (ny *ℤ dx)) ∙ + ( ap-add-ℤ + ( inv (left-negative-law-mul-ℤ nx dy)) + ( inv (left-negative-law-mul-ℤ ny dx)))) ``` diff --git a/src/elementary-number-theory/addition-integers.lagda.md b/src/elementary-number-theory/addition-integers.lagda.md index 0e17c532a8..51c6422199 100644 --- a/src/elementary-number-theory/addition-integers.lagda.md +++ b/src/elementary-number-theory/addition-integers.lagda.md @@ -330,36 +330,39 @@ abstract ### Interchange law for addition with respect to addition ```agda -interchange-law-add-add-ℤ : interchange-law add-ℤ add-ℤ -interchange-law-add-add-ℤ = - interchange-law-commutative-and-associative - add-ℤ - commutative-add-ℤ - associative-add-ℤ +abstract + interchange-law-add-add-ℤ : + (x y u v : ℤ) → (x +ℤ y) +ℤ (u +ℤ v) ＝ (x +ℤ u) +ℤ (y +ℤ v) + interchange-law-add-add-ℤ = + interchange-law-commutative-and-associative + add-ℤ + commutative-add-ℤ + associative-add-ℤ ``` ### Addition by `x` is a binary equivalence ```agda -is-section-left-add-neg-ℤ : - (x y : ℤ) → x +ℤ (neg-ℤ x +ℤ y) ＝ y -is-section-left-add-neg-ℤ x y = - equational-reasoning - x +ℤ (neg-ℤ x +ℤ y) - ＝ (x +ℤ neg-ℤ x) +ℤ y - by inv (associative-add-ℤ x (neg-ℤ x) y) - ＝ y - by ap (_+ℤ y) (right-inverse-law-add-ℤ x) - -is-retraction-left-add-neg-ℤ : - (x y : ℤ) → (neg-ℤ x) +ℤ (x +ℤ y) ＝ y -is-retraction-left-add-neg-ℤ x y = - equational-reasoning - neg-ℤ x +ℤ (x +ℤ y) - ＝ (neg-ℤ x +ℤ x) +ℤ y - by inv (associative-add-ℤ (neg-ℤ x) x y) - ＝ y - by ap (_+ℤ y) (left-inverse-law-add-ℤ x) +abstract + is-section-left-add-neg-ℤ : + (x y : ℤ) → x +ℤ (neg-ℤ x +ℤ y) ＝ y + is-section-left-add-neg-ℤ x y = + equational-reasoning + x +ℤ (neg-ℤ x +ℤ y) + ＝ (x +ℤ neg-ℤ x) +ℤ y + by inv (associative-add-ℤ x (neg-ℤ x) y) + ＝ y + by ap (_+ℤ y) (right-inverse-law-add-ℤ x) + + is-retraction-left-add-neg-ℤ : + (x y : ℤ) → (neg-ℤ x) +ℤ (x +ℤ y) ＝ y + is-retraction-left-add-neg-ℤ x y = + equational-reasoning + neg-ℤ x +ℤ (x +ℤ y) + ＝ (neg-ℤ x +ℤ x) +ℤ y + by inv (associative-add-ℤ (neg-ℤ x) x y) + ＝ y + by ap (_+ℤ y) (left-inverse-law-add-ℤ x) abstract is-equiv-left-add-ℤ : (x : ℤ) → is-equiv (x +ℤ_) @@ -372,29 +375,30 @@ equiv-left-add-ℤ : ℤ → (ℤ ≃ ℤ) pr1 (equiv-left-add-ℤ x) = add-ℤ x pr2 (equiv-left-add-ℤ x) = is-equiv-left-add-ℤ x -is-section-right-add-neg-ℤ : - (x y : ℤ) → (y +ℤ neg-ℤ x) +ℤ x ＝ y -is-section-right-add-neg-ℤ x y = - equational-reasoning - (y +ℤ neg-ℤ x) +ℤ x - ＝ y +ℤ (neg-ℤ x +ℤ x) - by associative-add-ℤ y (neg-ℤ x) x - ＝ y +ℤ zero-ℤ - by ap (y +ℤ_) (left-inverse-law-add-ℤ x) - ＝ y - by right-unit-law-add-ℤ y - -is-retraction-right-add-neg-ℤ : - (x y : ℤ) → (y +ℤ x) +ℤ neg-ℤ x ＝ y -is-retraction-right-add-neg-ℤ x y = - equational-reasoning - (y +ℤ x) +ℤ neg-ℤ x - ＝ y +ℤ (x +ℤ neg-ℤ x) - by associative-add-ℤ y x (neg-ℤ x) - ＝ y +ℤ zero-ℤ - by ap (y +ℤ_) (right-inverse-law-add-ℤ x) - ＝ y - by right-unit-law-add-ℤ y +abstract + is-section-right-add-neg-ℤ : + (x y : ℤ) → (y +ℤ neg-ℤ x) +ℤ x ＝ y + is-section-right-add-neg-ℤ x y = + equational-reasoning + (y +ℤ neg-ℤ x) +ℤ x + ＝ y +ℤ (neg-ℤ x +ℤ x) + by associative-add-ℤ y (neg-ℤ x) x + ＝ y +ℤ zero-ℤ + by ap (y +ℤ_) (left-inverse-law-add-ℤ x) + ＝ y + by right-unit-law-add-ℤ y + + is-retraction-right-add-neg-ℤ : + (x y : ℤ) → (y +ℤ x) +ℤ neg-ℤ x ＝ y + is-retraction-right-add-neg-ℤ x y = + equational-reasoning + (y +ℤ x) +ℤ neg-ℤ x + ＝ y +ℤ (x +ℤ neg-ℤ x) + by associative-add-ℤ y x (neg-ℤ x) + ＝ y +ℤ zero-ℤ + by ap (y +ℤ_) (right-inverse-law-add-ℤ x) + ＝ y + by right-unit-law-add-ℤ y abstract is-equiv-right-add-ℤ : (y : ℤ) → is-equiv (_+ℤ y) @@ -415,141 +419,152 @@ pr2 is-binary-equiv-left-add-ℤ = is-equiv-left-add-ℤ ### Addition by an integer is a binary embedding ```agda -is-emb-left-add-ℤ : - (x : ℤ) → is-emb (x +ℤ_) -is-emb-left-add-ℤ x = - is-emb-is-equiv (is-equiv-left-add-ℤ x) - -is-emb-right-add-ℤ : - (y : ℤ) → is-emb (_+ℤ y) -is-emb-right-add-ℤ y = is-emb-is-equiv (is-equiv-right-add-ℤ y) - -is-binary-emb-add-ℤ : is-binary-emb add-ℤ -is-binary-emb-add-ℤ = - is-binary-emb-is-binary-equiv is-binary-equiv-left-add-ℤ +abstract + is-emb-left-add-ℤ : + (x : ℤ) → is-emb (x +ℤ_) + is-emb-left-add-ℤ x = + is-emb-is-equiv (is-equiv-left-add-ℤ x) + + is-emb-right-add-ℤ : + (y : ℤ) → is-emb (_+ℤ y) + is-emb-right-add-ℤ y = is-emb-is-equiv (is-equiv-right-add-ℤ y) + + is-binary-emb-add-ℤ : is-binary-emb add-ℤ + is-binary-emb-add-ℤ = + is-binary-emb-is-binary-equiv is-binary-equiv-left-add-ℤ ``` ### Addition by `x` is injective ```agda -is-injective-right-add-ℤ : (x : ℤ) → is-injective (_+ℤ x) -is-injective-right-add-ℤ x = is-injective-is-emb (is-emb-right-add-ℤ x) +abstract + is-injective-right-add-ℤ : (x : ℤ) → is-injective (_+ℤ x) + is-injective-right-add-ℤ x = is-injective-is-emb (is-emb-right-add-ℤ x) -is-injective-add-ℤ : (x : ℤ) → is-injective (x +ℤ_) -is-injective-add-ℤ x = is-injective-is-emb (is-emb-left-add-ℤ x) + is-injective-left-add-ℤ : (x : ℤ) → is-injective (x +ℤ_) + is-injective-left-add-ℤ x = is-injective-is-emb (is-emb-left-add-ℤ x) ``` ### Negative laws for addition ```agda -right-negative-law-add-ℤ : - (k l : ℤ) → k +ℤ neg-ℤ l ＝ neg-ℤ (neg-ℤ k +ℤ l) -right-negative-law-add-ℤ (inl zero-ℕ) l = - equational-reasoning - neg-one-ℤ +ℤ neg-ℤ l - ＝ pred-ℤ (zero-ℤ +ℤ neg-ℤ l) - by left-predecessor-law-add-ℤ zero-ℤ (neg-ℤ l) - ＝ neg-ℤ (succ-ℤ l) - by pred-neg-ℤ l -right-negative-law-add-ℤ (inl (succ-ℕ x)) l = - equational-reasoning - pred-ℤ (inl x) +ℤ neg-ℤ l - ＝ pred-ℤ (inl x +ℤ neg-ℤ l) - by left-predecessor-law-add-ℤ (inl x) (neg-ℤ l) - ＝ pred-ℤ (neg-ℤ (neg-ℤ (inl x) +ℤ l)) - by ap pred-ℤ (right-negative-law-add-ℤ (inl x) l) - ＝ neg-ℤ (succ-ℤ (inr (inr x) +ℤ l)) - by pred-neg-ℤ (inr (inr x) +ℤ l) -right-negative-law-add-ℤ (inr (inl star)) l = - refl -right-negative-law-add-ℤ (inr (inr zero-ℕ)) l = - inv (neg-pred-ℤ l) -right-negative-law-add-ℤ (inr (inr (succ-ℕ n))) l = - equational-reasoning - succ-ℤ (in-pos n) +ℤ neg-ℤ l - ＝ succ-ℤ (in-pos n +ℤ neg-ℤ l) - by left-successor-law-add-ℤ (in-pos n) (neg-ℤ l) - ＝ succ-ℤ (neg-ℤ (neg-ℤ (inr (inr n)) +ℤ l)) - by ap succ-ℤ (right-negative-law-add-ℤ (inr (inr n)) l) - ＝ neg-ℤ (pred-ℤ ((inl n) +ℤ l)) - by inv (neg-pred-ℤ ((inl n) +ℤ l)) +abstract + right-negative-law-add-ℤ : + (k l : ℤ) → k +ℤ neg-ℤ l ＝ neg-ℤ (neg-ℤ k +ℤ l) + right-negative-law-add-ℤ (inl zero-ℕ) l = + equational-reasoning + neg-one-ℤ +ℤ neg-ℤ l + ＝ pred-ℤ (zero-ℤ +ℤ neg-ℤ l) + by left-predecessor-law-add-ℤ zero-ℤ (neg-ℤ l) + ＝ neg-ℤ (succ-ℤ l) + by pred-neg-ℤ l + right-negative-law-add-ℤ (inl (succ-ℕ x)) l = + equational-reasoning + pred-ℤ (inl x) +ℤ neg-ℤ l + ＝ pred-ℤ (inl x +ℤ neg-ℤ l) + by left-predecessor-law-add-ℤ (inl x) (neg-ℤ l) + ＝ pred-ℤ (neg-ℤ (neg-ℤ (inl x) +ℤ l)) + by ap pred-ℤ (right-negative-law-add-ℤ (inl x) l) + ＝ neg-ℤ (succ-ℤ (inr (inr x) +ℤ l)) + by pred-neg-ℤ (inr (inr x) +ℤ l) + right-negative-law-add-ℤ (inr (inl star)) l = + refl + right-negative-law-add-ℤ (inr (inr zero-ℕ)) l = + inv (neg-pred-ℤ l) + right-negative-law-add-ℤ (inr (inr (succ-ℕ n))) l = + equational-reasoning + succ-ℤ (in-pos-ℤ n) +ℤ neg-ℤ l + ＝ succ-ℤ (in-pos-ℤ n +ℤ neg-ℤ l) + by left-successor-law-add-ℤ (in-pos-ℤ n) (neg-ℤ l) + ＝ succ-ℤ (neg-ℤ (neg-ℤ (inr (inr n)) +ℤ l)) + by ap succ-ℤ (right-negative-law-add-ℤ (inr (inr n)) l) + ＝ neg-ℤ (pred-ℤ ((inl n) +ℤ l)) + by inv (neg-pred-ℤ ((inl n) +ℤ l)) ``` ### Distributivity of negatives over addition ```agda -distributive-neg-add-ℤ : - (k l : ℤ) → neg-ℤ (k +ℤ l) ＝ neg-ℤ k +ℤ neg-ℤ l -distributive-neg-add-ℤ (inl zero-ℕ) l = - equational-reasoning - neg-ℤ (inl zero-ℕ +ℤ l) - ＝ neg-ℤ (pred-ℤ (zero-ℤ +ℤ l)) - by ap neg-ℤ (left-predecessor-law-add-ℤ zero-ℤ l) - ＝ neg-ℤ (inl zero-ℕ) +ℤ neg-ℤ l - by neg-pred-ℤ l -distributive-neg-add-ℤ (inl (succ-ℕ n)) l = - equational-reasoning - neg-ℤ (pred-ℤ (inl n +ℤ l)) - ＝ succ-ℤ (neg-ℤ (inl n +ℤ l)) - by neg-pred-ℤ (inl n +ℤ l) - ＝ succ-ℤ (neg-ℤ (inl n) +ℤ neg-ℤ l) - by ap succ-ℤ (distributive-neg-add-ℤ (inl n) l) - ＝ neg-ℤ (pred-ℤ (inl n)) +ℤ neg-ℤ l - by ap (_+ℤ (neg-ℤ l)) (inv (neg-pred-ℤ (inl n))) -distributive-neg-add-ℤ (inr (inl star)) l = - refl -distributive-neg-add-ℤ (inr (inr zero-ℕ)) l = - inv (pred-neg-ℤ l) -distributive-neg-add-ℤ (inr (inr (succ-ℕ n))) l = - equational-reasoning - neg-ℤ (succ-ℤ (in-pos n +ℤ l)) - ＝ pred-ℤ (neg-ℤ (in-pos n +ℤ l)) - by inv (pred-neg-ℤ (in-pos n +ℤ l)) - ＝ pred-ℤ (neg-ℤ (inr (inr n)) +ℤ neg-ℤ l) - by ap pred-ℤ (distributive-neg-add-ℤ (inr (inr n)) l) +abstract + distributive-neg-add-ℤ : + (k l : ℤ) → neg-ℤ (k +ℤ l) ＝ neg-ℤ k +ℤ neg-ℤ l + distributive-neg-add-ℤ (inl zero-ℕ) l = + equational-reasoning + neg-ℤ (inl zero-ℕ +ℤ l) + ＝ neg-ℤ (pred-ℤ (zero-ℤ +ℤ l)) + by ap neg-ℤ (left-predecessor-law-add-ℤ zero-ℤ l) + ＝ neg-ℤ (inl zero-ℕ) +ℤ neg-ℤ l + by neg-pred-ℤ l + distributive-neg-add-ℤ (inl (succ-ℕ n)) l = + equational-reasoning + neg-ℤ (pred-ℤ (inl n +ℤ l)) + ＝ succ-ℤ (neg-ℤ (inl n +ℤ l)) + by neg-pred-ℤ (inl n +ℤ l) + ＝ succ-ℤ (neg-ℤ (inl n) +ℤ neg-ℤ l) + by ap succ-ℤ (distributive-neg-add-ℤ (inl n) l) + ＝ neg-ℤ (pred-ℤ (inl n)) +ℤ neg-ℤ l + by ap (_+ℤ (neg-ℤ l)) (inv (neg-pred-ℤ (inl n))) + distributive-neg-add-ℤ (inr (inl star)) l = + refl + distributive-neg-add-ℤ (inr (inr zero-ℕ)) l = + inv (pred-neg-ℤ l) + distributive-neg-add-ℤ (inr (inr (succ-ℕ n))) l = + equational-reasoning + neg-ℤ (succ-ℤ (in-pos-ℤ n +ℤ l)) + ＝ pred-ℤ (neg-ℤ (in-pos-ℤ n +ℤ l)) + by inv (pred-neg-ℤ (in-pos-ℤ n +ℤ l)) + ＝ pred-ℤ (neg-ℤ (inr (inr n)) +ℤ neg-ℤ l) + by ap pred-ℤ (distributive-neg-add-ℤ (inr (inr n)) l) ``` ### The inclusion of ℕ into ℤ preserves addition ```agda -add-int-ℕ : (x y : ℕ) → (int-ℕ x) +ℤ (int-ℕ y) ＝ int-ℕ (x +ℕ y) -add-int-ℕ x zero-ℕ = right-unit-law-add-ℤ (int-ℕ x) -add-int-ℕ x (succ-ℕ y) = - equational-reasoning - int-ℕ x +ℤ int-ℕ (succ-ℕ y) - ＝ int-ℕ x +ℤ succ-ℤ (int-ℕ y) - by ap ((int-ℕ x) +ℤ_) (inv (succ-int-ℕ y)) - ＝ succ-ℤ (int-ℕ x +ℤ int-ℕ y) - by right-successor-law-add-ℤ (int-ℕ x) (int-ℕ y) - ＝ succ-ℤ (int-ℕ (x +ℕ y)) - by ap succ-ℤ (add-int-ℕ x y) - ＝ int-ℕ (succ-ℕ (x +ℕ y)) - by succ-int-ℕ (x +ℕ y) +abstract + add-int-ℕ : (x y : ℕ) → (int-ℕ x) +ℤ (int-ℕ y) ＝ int-ℕ (x +ℕ y) + add-int-ℕ x zero-ℕ = right-unit-law-add-ℤ (int-ℕ x) + add-int-ℕ x (succ-ℕ y) = + equational-reasoning + int-ℕ x +ℤ int-ℕ (succ-ℕ y) + ＝ int-ℕ x +ℤ succ-ℤ (int-ℕ y) + by ap ((int-ℕ x) +ℤ_) (inv (succ-int-ℕ y)) + ＝ succ-ℤ (int-ℕ x +ℤ int-ℕ y) + by right-successor-law-add-ℤ (int-ℕ x) (int-ℕ y) + ＝ succ-ℤ (int-ℕ (x +ℕ y)) + by ap succ-ℤ (add-int-ℕ x y) + ＝ int-ℕ (succ-ℕ (x +ℕ y)) + by succ-int-ℕ (x +ℕ y) ``` ### If `x + y = y` then `x = 0` ```agda -is-zero-left-add-ℤ : - (x y : ℤ) → x +ℤ y ＝ y → is-zero-ℤ x -is-zero-left-add-ℤ x y H = - equational-reasoning - x - ＝ x +ℤ zero-ℤ - by inv (right-unit-law-add-ℤ x) - ＝ x +ℤ (y +ℤ neg-ℤ y) - by inv (ap (x +ℤ_) (right-inverse-law-add-ℤ y)) - ＝ (x +ℤ y) +ℤ neg-ℤ y - by inv (associative-add-ℤ x y (neg-ℤ y)) - ＝ y +ℤ neg-ℤ y - by ap (_+ℤ (neg-ℤ y)) H - ＝ zero-ℤ - by right-inverse-law-add-ℤ y - -is-zero-right-add-ℤ : - (x y : ℤ) → x +ℤ y ＝ x → is-zero-ℤ y -is-zero-right-add-ℤ x y H = - is-zero-left-add-ℤ y x (commutative-add-ℤ y x ∙ H) +abstract + is-zero-left-add-ℤ : + (x y : ℤ) → x +ℤ y ＝ y → is-zero-ℤ x + is-zero-left-add-ℤ x y H = + equational-reasoning + x + ＝ x +ℤ zero-ℤ + by inv (right-unit-law-add-ℤ x) + ＝ x +ℤ (y +ℤ neg-ℤ y) + by inv (ap (x +ℤ_) (right-inverse-law-add-ℤ y)) + ＝ (x +ℤ y) +ℤ neg-ℤ y + by inv (associative-add-ℤ x y (neg-ℤ y)) + ＝ y +ℤ neg-ℤ y + by ap (_+ℤ (neg-ℤ y)) H + ＝ zero-ℤ + by right-inverse-law-add-ℤ y +``` + +### If `x + y = x` then `y = 0` + +```agda +abstract + is-zero-right-add-ℤ : + (x y : ℤ) → x +ℤ y ＝ x → is-zero-ℤ y + is-zero-right-add-ℤ x y H = + is-zero-left-add-ℤ y x (commutative-add-ℤ y x ∙ H) ``` ## See also diff --git a/src/elementary-number-theory/addition-natural-numbers.lagda.md b/src/elementary-number-theory/addition-natural-numbers.lagda.md index 961a1566d1..403385d149 100644 --- a/src/elementary-number-theory/addition-natural-numbers.lagda.md +++ b/src/elementary-number-theory/addition-natural-numbers.lagda.md @@ -61,11 +61,12 @@ left-unit-law-add-ℕ (succ-ℕ x) = ap succ-ℕ (left-unit-law-add-ℕ x) ### The left and right successor laws ```agda -left-successor-law-add-ℕ : - (x y : ℕ) → (succ-ℕ x) +ℕ y ＝ succ-ℕ (x +ℕ y) -left-successor-law-add-ℕ x zero-ℕ = refl -left-successor-law-add-ℕ x (succ-ℕ y) = - ap succ-ℕ (left-successor-law-add-ℕ x y) +abstract + left-successor-law-add-ℕ : + (x y : ℕ) → (succ-ℕ x) +ℕ y ＝ succ-ℕ (x +ℕ y) + left-successor-law-add-ℕ x zero-ℕ = refl + left-successor-law-add-ℕ x (succ-ℕ y) = + ap succ-ℕ (left-successor-law-add-ℕ x y) right-successor-law-add-ℕ : (x y : ℕ) → x +ℕ (succ-ℕ y) ＝ succ-ℕ (x +ℕ y) @@ -75,118 +76,129 @@ right-successor-law-add-ℕ x y = refl ### Addition is associative ```agda -associative-add-ℕ : - (x y z : ℕ) → (x +ℕ y) +ℕ z ＝ x +ℕ (y +ℕ z) -associative-add-ℕ x y zero-ℕ = refl -associative-add-ℕ x y (succ-ℕ z) = ap succ-ℕ (associative-add-ℕ x y z) +abstract + associative-add-ℕ : + (x y z : ℕ) → (x +ℕ y) +ℕ z ＝ x +ℕ (y +ℕ z) + associative-add-ℕ x y zero-ℕ = refl + associative-add-ℕ x y (succ-ℕ z) = ap succ-ℕ (associative-add-ℕ x y z) ``` ### Addition is commutative ```agda -commutative-add-ℕ : (x y : ℕ) → x +ℕ y ＝ y +ℕ x -commutative-add-ℕ zero-ℕ y = left-unit-law-add-ℕ y -commutative-add-ℕ (succ-ℕ x) y = - (left-successor-law-add-ℕ x y) ∙ (ap succ-ℕ (commutative-add-ℕ x y)) +abstract + commutative-add-ℕ : (x y : ℕ) → x +ℕ y ＝ y +ℕ x + commutative-add-ℕ zero-ℕ y = left-unit-law-add-ℕ y + commutative-add-ℕ (succ-ℕ x) y = + (left-successor-law-add-ℕ x y) ∙ (ap succ-ℕ (commutative-add-ℕ x y)) ``` ### Addition by `1` on the left or on the right is the successor ```agda -left-one-law-add-ℕ : - (x : ℕ) → 1 +ℕ x ＝ succ-ℕ x -left-one-law-add-ℕ x = - ( left-successor-law-add-ℕ zero-ℕ x) ∙ - ( ap succ-ℕ (left-unit-law-add-ℕ x)) - -right-one-law-add-ℕ : - (x : ℕ) → x +ℕ 1 ＝ succ-ℕ x -right-one-law-add-ℕ x = refl +abstract + left-one-law-add-ℕ : + (x : ℕ) → 1 +ℕ x ＝ succ-ℕ x + left-one-law-add-ℕ x = + ( left-successor-law-add-ℕ zero-ℕ x) ∙ + ( ap succ-ℕ (left-unit-law-add-ℕ x)) + + right-one-law-add-ℕ : + (x : ℕ) → x +ℕ 1 ＝ succ-ℕ x + right-one-law-add-ℕ x = refl ``` ### Addition by `1` on the left or on the right is the double successor ```agda -left-two-law-add-ℕ : - (x : ℕ) → 2 +ℕ x ＝ succ-ℕ (succ-ℕ x) -left-two-law-add-ℕ x = - ( left-successor-law-add-ℕ 1 x) ∙ - ( ap succ-ℕ (left-one-law-add-ℕ x)) - -right-two-law-add-ℕ : - (x : ℕ) → x +ℕ 2 ＝ succ-ℕ (succ-ℕ x) -right-two-law-add-ℕ x = refl +abstract + left-two-law-add-ℕ : + (x : ℕ) → 2 +ℕ x ＝ succ-ℕ (succ-ℕ x) + left-two-law-add-ℕ x = + ( left-successor-law-add-ℕ 1 x) ∙ + ( ap succ-ℕ (left-one-law-add-ℕ x)) + + right-two-law-add-ℕ : + (x : ℕ) → x +ℕ 2 ＝ succ-ℕ (succ-ℕ x) + right-two-law-add-ℕ x = refl ``` ### Interchange law of addition ```agda -interchange-law-add-add-ℕ : interchange-law add-ℕ add-ℕ -interchange-law-add-add-ℕ = - interchange-law-commutative-and-associative - add-ℕ - commutative-add-ℕ - associative-add-ℕ +abstract + interchange-law-add-add-ℕ : interchange-law add-ℕ add-ℕ + interchange-law-add-add-ℕ = + interchange-law-commutative-and-associative + add-ℕ + commutative-add-ℕ + associative-add-ℕ ``` ### Addition by a fixed element on either side is injective ```agda -is-injective-right-add-ℕ : (k : ℕ) → is-injective (_+ℕ k) -is-injective-right-add-ℕ zero-ℕ = id -is-injective-right-add-ℕ (succ-ℕ k) p = - is-injective-right-add-ℕ k (is-injective-succ-ℕ p) - -is-injective-left-add-ℕ : (k : ℕ) → is-injective (k +ℕ_) -is-injective-left-add-ℕ k {x} {y} p = - is-injective-right-add-ℕ - ( k) - ( commutative-add-ℕ x k ∙ (p ∙ commutative-add-ℕ k y)) +abstract + is-injective-right-add-ℕ : (k : ℕ) → is-injective (_+ℕ k) + is-injective-right-add-ℕ zero-ℕ = id + is-injective-right-add-ℕ (succ-ℕ k) p = + is-injective-right-add-ℕ k (is-injective-succ-ℕ p) + + is-injective-left-add-ℕ : (k : ℕ) → is-injective (k +ℕ_) + is-injective-left-add-ℕ k {x} {y} p = + is-injective-right-add-ℕ + ( k) + ( commutative-add-ℕ x k ∙ (p ∙ commutative-add-ℕ k y)) ``` ### Addition by a fixed element on either side is an embedding ```agda -is-emb-left-add-ℕ : (x : ℕ) → is-emb (x +ℕ_) -is-emb-left-add-ℕ x = is-emb-is-injective is-set-ℕ (is-injective-left-add-ℕ x) - -is-emb-right-add-ℕ : (x : ℕ) → is-emb (_+ℕ x) -is-emb-right-add-ℕ x = is-emb-is-injective is-set-ℕ (is-injective-right-add-ℕ x) +abstract + is-emb-left-add-ℕ : (x : ℕ) → is-emb (x +ℕ_) + is-emb-left-add-ℕ x = + is-emb-is-injective is-set-ℕ (is-injective-left-add-ℕ x) + + is-emb-right-add-ℕ : (x : ℕ) → is-emb (_+ℕ x) + is-emb-right-add-ℕ x = + is-emb-is-injective is-set-ℕ (is-injective-right-add-ℕ x) ``` ### `x + y ＝ 0` if and only if both `x` and `y` are `0` ```agda -is-zero-right-is-zero-add-ℕ : - (x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ y -is-zero-right-is-zero-add-ℕ x zero-ℕ p = refl -is-zero-right-is-zero-add-ℕ x (succ-ℕ y) p = - ex-falso (is-nonzero-succ-ℕ (x +ℕ y) p) - -is-zero-left-is-zero-add-ℕ : - (x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ x -is-zero-left-is-zero-add-ℕ x y p = - is-zero-right-is-zero-add-ℕ y x ((commutative-add-ℕ y x) ∙ p) - -is-zero-summand-is-zero-sum-ℕ : - (x y : ℕ) → is-zero-ℕ (x +ℕ y) → (is-zero-ℕ x) × (is-zero-ℕ y) -is-zero-summand-is-zero-sum-ℕ x y p = - pair (is-zero-left-is-zero-add-ℕ x y p) (is-zero-right-is-zero-add-ℕ x y p) - -is-zero-sum-is-zero-summand-ℕ : - (x y : ℕ) → (is-zero-ℕ x) × (is-zero-ℕ y) → is-zero-ℕ (x +ℕ y) -is-zero-sum-is-zero-summand-ℕ .zero-ℕ .zero-ℕ (pair refl refl) = refl +abstract + is-zero-right-is-zero-add-ℕ : + (x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ y + is-zero-right-is-zero-add-ℕ x zero-ℕ p = refl + is-zero-right-is-zero-add-ℕ x (succ-ℕ y) p = + ex-falso (is-nonzero-succ-ℕ (x +ℕ y) p) + + is-zero-left-is-zero-add-ℕ : + (x y : ℕ) → is-zero-ℕ (x +ℕ y) → is-zero-ℕ x + is-zero-left-is-zero-add-ℕ x y p = + is-zero-right-is-zero-add-ℕ y x ((commutative-add-ℕ y x) ∙ p) + + is-zero-summand-is-zero-sum-ℕ : + (x y : ℕ) → is-zero-ℕ (x +ℕ y) → (is-zero-ℕ x) × (is-zero-ℕ y) + is-zero-summand-is-zero-sum-ℕ x y p = + pair (is-zero-left-is-zero-add-ℕ x y p) (is-zero-right-is-zero-add-ℕ x y p) + + is-zero-sum-is-zero-summand-ℕ : + (x y : ℕ) → (is-zero-ℕ x) × (is-zero-ℕ y) → is-zero-ℕ (x +ℕ y) + is-zero-sum-is-zero-summand-ℕ .zero-ℕ .zero-ℕ (pair refl refl) = refl ``` ### `m ≠ m + n + 1` ```agda -neq-add-ℕ : - (m n : ℕ) → m ≠ m +ℕ (succ-ℕ n) -neq-add-ℕ (succ-ℕ m) n p = - neq-add-ℕ m n - ( ( is-injective-succ-ℕ p) ∙ - ( left-successor-law-add-ℕ m n)) +abstract + neq-add-ℕ : + (m n : ℕ) → m ≠ m +ℕ (succ-ℕ n) + neq-add-ℕ (succ-ℕ m) n p = + neq-add-ℕ m n + ( ( is-injective-succ-ℕ p) ∙ + ( left-successor-law-add-ℕ m n)) ``` ## See also diff --git a/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md index ae0daa642c..cc38778380 100644 --- a/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md +++ b/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md @@ -56,110 +56,118 @@ displays the corresponding Agda definition. ### The sum of two positive integers is positive ```agda -is-positive-add-ℤ : - {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-ℤ {inr (inr zero-ℕ)} {y} H K = - is-positive-succ-is-positive-ℤ K -is-positive-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = - is-positive-succ-is-positive-ℤ - ( is-positive-add-ℤ {inr (inr x)} H K) +abstract + is-positive-add-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) + is-positive-add-ℤ {inr (inr zero-ℕ)} {y} H K = + is-positive-succ-is-positive-ℤ K + is-positive-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-positive-succ-is-positive-ℤ + ( is-positive-add-ℤ {inr (inr x)} H K) ``` ### The sum of a positive and a nonnegative integer is positive ```agda -is-positive-add-positive-nonnegative-ℤ : - {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K = - is-positive-succ-is-nonnegative-ℤ K -is-positive-add-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K = - is-positive-succ-is-positive-ℤ - ( is-positive-add-positive-nonnegative-ℤ {inr (inr x)} H K) +abstract + is-positive-add-positive-nonnegative-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y) + is-positive-add-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K = + is-positive-succ-is-nonnegative-ℤ K + is-positive-add-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-positive-succ-is-positive-ℤ + ( is-positive-add-positive-nonnegative-ℤ {inr (inr x)} H K) ``` ### The sum of a nonnegative and a positive integer is positive ```agda -is-positive-add-nonnegative-positive-ℤ : - {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-nonnegative-positive-ℤ {x} {y} H K = - is-positive-eq-ℤ - ( commutative-add-ℤ y x) - ( is-positive-add-positive-nonnegative-ℤ K H) +abstract + is-positive-add-nonnegative-positive-ℤ : + {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) + is-positive-add-nonnegative-positive-ℤ {x} {y} H K = + is-positive-eq-ℤ + ( commutative-add-ℤ y x) + ( is-positive-add-positive-nonnegative-ℤ K H) ``` ### The sum of two nonnegative integers is nonnegative ```agda -is-nonnegative-add-ℤ : - {x y : ℤ} → - is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x +ℤ y) -is-nonnegative-add-ℤ {inr (inl x)} {y} H K = K -is-nonnegative-add-ℤ {inr (inr zero-ℕ)} {y} H K = - is-nonnegative-succ-is-nonnegative-ℤ K -is-nonnegative-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = - is-nonnegative-succ-is-nonnegative-ℤ - ( is-nonnegative-add-ℤ {inr (inr x)} star K) +abstract + is-nonnegative-add-ℤ : + {x y : ℤ} → + is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x +ℤ y) + is-nonnegative-add-ℤ {inr (inl x)} {y} H K = K + is-nonnegative-add-ℤ {inr (inr zero-ℕ)} {y} H K = + is-nonnegative-succ-is-nonnegative-ℤ K + is-nonnegative-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-nonnegative-succ-is-nonnegative-ℤ + ( is-nonnegative-add-ℤ {inr (inr x)} star K) ``` ### The sum of two negative integers is negative ```agda -is-negative-add-ℤ : - {x y : ℤ} → is-negative-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) -is-negative-add-ℤ {x} {y} H K = - is-negative-eq-ℤ - ( neg-neg-ℤ (x +ℤ y)) - ( is-negative-neg-is-positive-ℤ - ( is-positive-eq-ℤ - ( inv (distributive-neg-add-ℤ x y)) - ( is-positive-add-ℤ - ( is-positive-neg-is-negative-ℤ H) - ( is-positive-neg-is-negative-ℤ K)))) +abstract + is-negative-add-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) + is-negative-add-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-negative-neg-is-positive-ℤ + ( is-positive-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-positive-add-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-positive-neg-is-negative-ℤ K)))) ``` ### The sum of a negative and a nonpositive integer is negative ```agda -is-negative-add-negative-nonnegative-ℤ : - {x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-negative-ℤ (x +ℤ y) -is-negative-add-negative-nonnegative-ℤ {x} {y} H K = - is-negative-eq-ℤ - ( neg-neg-ℤ (x +ℤ y)) - ( is-negative-neg-is-positive-ℤ - ( is-positive-eq-ℤ - ( inv (distributive-neg-add-ℤ x y)) - ( is-positive-add-positive-nonnegative-ℤ - ( is-positive-neg-is-negative-ℤ H) - ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +abstract + is-negative-add-negative-nonnegative-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-negative-ℤ (x +ℤ y) + is-negative-add-negative-nonnegative-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-negative-neg-is-positive-ℤ + ( is-positive-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-positive-add-positive-nonnegative-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) ``` ### The sum of a nonpositive and a negative integer is negative ```agda -is-negative-add-nonpositive-negative-ℤ : - {x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) -is-negative-add-nonpositive-negative-ℤ {x} {y} H K = - is-negative-eq-ℤ - ( commutative-add-ℤ y x) - ( is-negative-add-negative-nonnegative-ℤ K H) +abstract + is-negative-add-nonpositive-negative-ℤ : + {x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) + is-negative-add-nonpositive-negative-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( commutative-add-ℤ y x) + ( is-negative-add-negative-nonnegative-ℤ K H) ``` ### The sum of two nonpositive integers is nonpositive ```agda -is-nonpositive-add-ℤ : - {x y : ℤ} → - is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x +ℤ y) -is-nonpositive-add-ℤ {x} {y} H K = - is-nonpositive-eq-ℤ - ( neg-neg-ℤ (x +ℤ y)) - ( is-nonpositive-neg-is-nonnegative-ℤ - ( is-nonnegative-eq-ℤ - ( inv (distributive-neg-add-ℤ x y)) - ( is-nonnegative-add-ℤ - ( is-nonnegative-neg-is-nonpositive-ℤ H) - ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +abstract + is-nonpositive-add-ℤ : + {x y : ℤ} → + is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x +ℤ y) + is-nonpositive-add-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-nonnegative-add-ℤ + ( is-nonnegative-neg-is-nonpositive-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) ``` ## Definitions diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md index f653c99ef3..54ded78bf8 100644 --- a/src/elementary-number-theory/addition-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md @@ -15,23 +15,26 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.reduced-integer-fractions open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.interchange-law ``` ## Idea -We introduce addition on the rationals and derive its basic properties. -Properties of addition with respect to inequality are derived in -`inequality-rationals`. +We introduce +{{#concept "addition" Disambiguation="rational numbers" Agda=add-ℚ}} on the +[rational numbers](elementary-number-theory.rational-numbers.md) and derive its +basic properties. ## Definition ```agda add-ℚ : ℚ → ℚ → ℚ -add-ℚ (x , p) (y , q) = in-fraction-ℤ (add-fraction-ℤ x y) +add-ℚ (x , p) (y , q) = rational-fraction-ℤ (add-fraction-ℤ x y) add-ℚ' : ℚ → ℚ → ℚ add-ℚ' x y = add-ℚ y x @@ -49,57 +52,114 @@ ap-add-ℚ p q = ap-binary add-ℚ p q ### Unit laws ```agda -left-unit-law-add-ℚ : (x : ℚ) → zero-ℚ +ℚ x ＝ x -left-unit-law-add-ℚ (x , p) = - eq-ℚ-sim-fraction-ℤ - ( add-fraction-ℤ zero-fraction-ℤ x) - ( x) - ( left-unit-law-add-fraction-ℤ x) ∙ - in-fraction-fraction-ℚ (x , p) - -right-unit-law-add-ℚ : (x : ℚ) → x +ℚ zero-ℚ ＝ x -right-unit-law-add-ℚ (x , p) = - eq-ℚ-sim-fraction-ℤ - ( add-fraction-ℤ x zero-fraction-ℤ) - ( x) - ( right-unit-law-add-fraction-ℤ x) ∙ - in-fraction-fraction-ℚ (x , p) +abstract + left-unit-law-add-ℚ : (x : ℚ) → zero-ℚ +ℚ x ＝ x + left-unit-law-add-ℚ (x , p) = + eq-ℚ-sim-fraction-ℤ + ( add-fraction-ℤ zero-fraction-ℤ x) + ( x) + ( left-unit-law-add-fraction-ℤ x) ∙ + is-retraction-rational-fraction-ℚ (x , p) + + right-unit-law-add-ℚ : (x : ℚ) → x +ℚ zero-ℚ ＝ x + right-unit-law-add-ℚ (x , p) = + eq-ℚ-sim-fraction-ℤ + ( add-fraction-ℤ x zero-fraction-ℤ) + ( x) + ( right-unit-law-add-fraction-ℤ x) ∙ + is-retraction-rational-fraction-ℚ (x , p) ``` ### Addition is associative ```agda -associative-add-ℚ : - (x y z : ℚ) → - (x +ℚ y) +ℚ z ＝ x +ℚ (y +ℚ z) -associative-add-ℚ (x , px) (y , py) (z , pz) = - equational-reasoning - in-fraction-ℤ (add-fraction-ℤ (pr1 (in-fraction-ℤ (add-fraction-ℤ x y))) z) - ＝ in-fraction-ℤ (add-fraction-ℤ (add-fraction-ℤ x y) z) - by eq-ℚ-sim-fraction-ℤ _ _ - ( sim-fraction-add-fraction-ℤ - ( symmetric-sim-fraction-ℤ _ _ - ( sim-reduced-fraction-ℤ (add-fraction-ℤ x y))) - ( refl-sim-fraction-ℤ z)) - ＝ in-fraction-ℤ (add-fraction-ℤ x (add-fraction-ℤ y z)) - by eq-ℚ-sim-fraction-ℤ _ _ (associative-add-fraction-ℤ x y z) - ＝ in-fraction-ℤ - ( add-fraction-ℤ x (pr1 (in-fraction-ℤ (add-fraction-ℤ y z)))) - by eq-ℚ-sim-fraction-ℤ _ _ - ( sim-fraction-add-fraction-ℤ - ( refl-sim-fraction-ℤ x) - ( sim-reduced-fraction-ℤ (add-fraction-ℤ y z))) +abstract + associative-add-ℚ : + (x y z : ℚ) → + (x +ℚ y) +ℚ z ＝ x +ℚ (y +ℚ z) + associative-add-ℚ (x , px) (y , py) (z , pz) = + equational-reasoning + rational-fraction-ℤ + (add-fraction-ℤ (pr1 (rational-fraction-ℤ (add-fraction-ℤ x y))) z) + ＝ rational-fraction-ℤ (add-fraction-ℤ (add-fraction-ℤ x y) z) + by eq-ℚ-sim-fraction-ℤ _ _ + ( sim-fraction-add-fraction-ℤ + ( symmetric-sim-fraction-ℤ _ _ + ( sim-reduced-fraction-ℤ (add-fraction-ℤ x y))) + ( refl-sim-fraction-ℤ z)) + ＝ rational-fraction-ℤ (add-fraction-ℤ x (add-fraction-ℤ y z)) + by eq-ℚ-sim-fraction-ℤ _ _ (associative-add-fraction-ℤ x y z) + ＝ rational-fraction-ℤ + ( add-fraction-ℤ x (pr1 (rational-fraction-ℤ (add-fraction-ℤ y z)))) + by eq-ℚ-sim-fraction-ℤ _ _ + ( sim-fraction-add-fraction-ℤ + ( refl-sim-fraction-ℤ x) + ( sim-reduced-fraction-ℤ (add-fraction-ℤ y z))) ``` ### Addition is commutative ```agda -commutative-add-ℚ : - (x y : ℚ) → - x +ℚ y ＝ y +ℚ x -commutative-add-ℚ (x , px) (y , py) = - eq-ℚ-sim-fraction-ℤ - ( add-fraction-ℤ x y) - ( add-fraction-ℤ y x) - ( commutative-add-fraction-ℤ x y) +abstract + commutative-add-ℚ : + (x y : ℚ) → + x +ℚ y ＝ y +ℚ x + commutative-add-ℚ (x , px) (y , py) = + eq-ℚ-sim-fraction-ℤ + ( add-fraction-ℤ x y) + ( add-fraction-ℤ y x) + ( commutative-add-fraction-ℤ x y) ``` + +### Interchange law for addition with respect to addition + +```agda +abstract + interchange-law-add-add-ℚ : + (x y u v : ℚ) → (x +ℚ y) +ℚ (u +ℚ v) ＝ (x +ℚ u) +ℚ (y +ℚ v) + interchange-law-add-add-ℚ = + interchange-law-commutative-and-associative + add-ℚ + commutative-add-ℚ + associative-add-ℚ +``` + +### The negative of a rational number is its additive inverse + +```agda +abstract + left-inverse-law-add-ℚ : (x : ℚ) → (neg-ℚ x) +ℚ x ＝ zero-ℚ + left-inverse-law-add-ℚ x = + ( eq-ℚ-sim-fraction-ℤ + ( add-fraction-ℤ (neg-fraction-ℤ (fraction-ℚ x)) (fraction-ℚ x)) + ( fraction-ℚ zero-ℚ) + ( sim-is-zero-numerator-fraction-ℤ + ( add-fraction-ℤ (neg-fraction-ℤ (fraction-ℚ x)) (fraction-ℚ x)) + ( fraction-ℚ zero-ℚ) + ( is-zero-numerator-add-left-neg-fraction-ℤ (fraction-ℚ x)) + ( refl))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) + + right-inverse-law-add-ℚ : (x : ℚ) → x +ℚ (neg-ℚ x) ＝ zero-ℚ + right-inverse-law-add-ℚ x = + commutative-add-ℚ x (neg-ℚ x) ∙ left-inverse-law-add-ℚ x +``` + +### The negatives of rational numbers distribute over addition + +```agda +abstract + distributive-neg-add-ℚ : + (x y : ℚ) → neg-ℚ (x +ℚ y) ＝ neg-ℚ x +ℚ neg-ℚ y + distributive-neg-add-ℚ (x , dxp) (y , dyp) = + ( inv (preserves-neg-rational-fraction-ℤ (x +fraction-ℤ y))) ∙ + ( eq-ℚ-sim-fraction-ℤ + ( neg-fraction-ℤ (x +fraction-ℤ y)) + ( add-fraction-ℤ (neg-fraction-ℤ x) (neg-fraction-ℤ y)) + ( distributive-neg-add-fraction-ℤ x y)) +``` + +## See also + +- The additive group structure on the rational numbers is defined in + [elementary-number-theory.group-of-rational-numbers.md]. diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md index 8bab982a09..2347b1a20e 100644 --- a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md +++ b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md @@ -317,7 +317,7 @@ bezouts-lemma-ℤ (inl x) (inr (inl star)) = pair neg-one-ℤ (pair one-ℤ eqn) by ap ( _+ℤ (one-ℤ *ℤ (inr (inl star)))) - ( inv (is-left-mul-neg-one-neg-ℤ (inl x))) + ( left-neg-unit-law-mul-ℤ (inl x)) ＝ (inr (inr x)) +ℤ zero-ℤ by ap ((inr (inr x)) +ℤ_) (right-zero-law-mul-ℤ one-ℤ) ＝ int-ℕ (abs-ℤ (inl x)) @@ -363,7 +363,7 @@ bezouts-lemma-ℤ (inr (inl star)) (inl y) = pair one-ℤ (pair neg-one-ℤ eqn) by ap ( (one-ℤ *ℤ (inr (inl star))) +ℤ_) - ( inv (is-left-mul-neg-one-neg-ℤ (inl y))) + ( left-neg-unit-law-mul-ℤ (inl y)) ＝ zero-ℤ +ℤ (inr (inr y)) by ap (_+ℤ (inr (inr y))) (right-zero-law-mul-ℤ one-ℤ) ＝ int-ℕ (abs-ℤ (inl y)) diff --git a/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md index 8fb4af6bbc..240bd25457 100644 --- a/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md +++ b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md @@ -108,8 +108,8 @@ lemma-add-cross-mul-diff-fraction-ℤ (dr *ℤ (nq *ℤ dp) -ℤ dr *ℤ (np *ℤ dq)) by ap-add-ℤ - ( inv (linear-diff-left-mul-ℤ dp (nr *ℤ dq) (nq *ℤ dr))) - ( inv (linear-diff-left-mul-ℤ dr (nq *ℤ dp) (np *ℤ dq))) + ( left-distributive-mul-diff-ℤ dp (nr *ℤ dq) (nq *ℤ dr)) + ( left-distributive-mul-diff-ℤ dr (nq *ℤ dp) (np *ℤ dq)) ＝ diff-ℤ (dp *ℤ (nr *ℤ dq) +ℤ dr *ℤ (nq *ℤ dp)) (dp *ℤ (nq *ℤ dr) +ℤ dr *ℤ (np *ℤ dq)) @@ -144,7 +144,7 @@ lemma-add-cross-mul-diff-fraction-ℤ (dq *ℤ (np *ℤ dr)) (dr *ℤ (nq *ℤ dp)) ＝ dq *ℤ (nr *ℤ dp -ℤ np *ℤ dr) - by linear-diff-left-mul-ℤ dq (nr *ℤ dp) (np *ℤ dr) + by inv (left-distributive-mul-diff-ℤ dq (nr *ℤ dp) (np *ℤ dr)) where lemma-interchange-mul-ℤ : (a b c : ℤ) → (a *ℤ (b *ℤ c)) ＝ (c *ℤ (b *ℤ a)) lemma-interchange-mul-ℤ a b c = diff --git a/src/elementary-number-theory/difference-integers.lagda.md b/src/elementary-number-theory/difference-integers.lagda.md index 759cd1ea0d..6cd796526c 100644 --- a/src/elementary-number-theory/difference-integers.lagda.md +++ b/src/elementary-number-theory/difference-integers.lagda.md @@ -33,97 +33,149 @@ diff-ℤ x y = x +ℤ (neg-ℤ y) infixl 36 _-ℤ_ _-ℤ_ = diff-ℤ + +ap-diff-ℤ : {x x' y y' : ℤ} → x ＝ x' → y ＝ y' → x -ℤ y ＝ x' -ℤ y' +ap-diff-ℤ p q = ap-binary diff-ℤ p q ``` ## Properties +### Two integers with a difference equal to zero are equal + ```agda -ap-diff-ℤ : {x x' y y' : ℤ} → x ＝ x' → y ＝ y' → x -ℤ y ＝ x' -ℤ y' -ap-diff-ℤ p q = ap-binary diff-ℤ p q +abstract + eq-diff-ℤ : {x y : ℤ} → is-zero-ℤ (x -ℤ y) → x ＝ y + eq-diff-ℤ {x} {y} H = + ( inv (right-unit-law-add-ℤ x)) ∙ + ( ap (x +ℤ_) (inv (left-inverse-law-add-ℤ y))) ∙ + ( inv (associative-add-ℤ x (neg-ℤ y) y)) ∙ + ( ap (_+ℤ y) H) ∙ + ( left-unit-law-add-ℤ y) +``` + +### The difference of an integer with itself is zero + +```agda +abstract + is-zero-diff-ℤ' : (x : ℤ) → is-zero-ℤ (x -ℤ x) + is-zero-diff-ℤ' = right-inverse-law-add-ℤ +``` + +### The difference of two equal integers is zero + +```agda +abstract + is-zero-diff-ℤ : {x y : ℤ} → x ＝ y → is-zero-ℤ (x -ℤ y) + is-zero-diff-ℤ {x} {.x} refl = is-zero-diff-ℤ' x +``` + +### The difference of zero and an integer is its negative + +```agda +abstract + left-zero-law-diff-ℤ : (x : ℤ) → zero-ℤ -ℤ x ＝ neg-ℤ x + left-zero-law-diff-ℤ x = left-unit-law-add-ℤ (neg-ℤ x) +``` + +### The difference of an integer with zero is itself + +```agda +abstract + right-zero-law-diff-ℤ : (x : ℤ) → x -ℤ zero-ℤ ＝ x + right-zero-law-diff-ℤ x = right-unit-law-add-ℤ x +``` + +### Differences with the predecessor or successor of an integer -eq-diff-ℤ : {x y : ℤ} → is-zero-ℤ (x -ℤ y) → x ＝ y -eq-diff-ℤ {x} {y} H = - ( inv (right-unit-law-add-ℤ x)) ∙ - ( ( ap (x +ℤ_) (inv (left-inverse-law-add-ℤ y))) ∙ - ( ( inv (associative-add-ℤ x (neg-ℤ y) y)) ∙ - ( ( ap (_+ℤ y) H) ∙ - ( left-unit-law-add-ℤ y)))) - -is-zero-diff-ℤ' : (x : ℤ) → is-zero-ℤ (x -ℤ x) -is-zero-diff-ℤ' = right-inverse-law-add-ℤ - -is-zero-diff-ℤ : - {x y : ℤ} → x ＝ y → is-zero-ℤ (x -ℤ y) -is-zero-diff-ℤ {x} {.x} refl = is-zero-diff-ℤ' x - -left-zero-law-diff-ℤ : (x : ℤ) → zero-ℤ -ℤ x ＝ neg-ℤ x -left-zero-law-diff-ℤ x = left-unit-law-add-ℤ (neg-ℤ x) - -right-zero-law-diff-ℤ : (x : ℤ) → x -ℤ zero-ℤ ＝ x -right-zero-law-diff-ℤ x = right-unit-law-add-ℤ x - -left-successor-law-diff-ℤ : - (x y : ℤ) → (succ-ℤ x) -ℤ y ＝ succ-ℤ (x -ℤ y) -left-successor-law-diff-ℤ x y = left-successor-law-add-ℤ x (neg-ℤ y) - -right-successor-law-diff-ℤ : - (x y : ℤ) → x -ℤ (succ-ℤ y) ＝ pred-ℤ (x -ℤ y) -right-successor-law-diff-ℤ x y = - ap (x +ℤ_) (neg-succ-ℤ y) ∙ right-predecessor-law-add-ℤ x (neg-ℤ y) - -left-predecessor-law-diff-ℤ : - (x y : ℤ) → (pred-ℤ x) -ℤ y ＝ pred-ℤ (x -ℤ y) -left-predecessor-law-diff-ℤ x y = left-predecessor-law-add-ℤ x (neg-ℤ y) - -right-predecessor-law-diff-ℤ : - (x y : ℤ) → x -ℤ (pred-ℤ y) ＝ succ-ℤ (x -ℤ y) -right-predecessor-law-diff-ℤ x y = - ap (x +ℤ_) (neg-pred-ℤ y) ∙ right-successor-law-add-ℤ x (neg-ℤ y) - -triangle-diff-ℤ : - (x y z : ℤ) → (x -ℤ y) +ℤ (y -ℤ z) ＝ x -ℤ z -triangle-diff-ℤ x y z = - ( associative-add-ℤ x (neg-ℤ y) (y -ℤ z)) ∙ - ( ap - ( x +ℤ_) - ( ( inv (associative-add-ℤ (neg-ℤ y) y (neg-ℤ z))) ∙ - ( ( ap (_+ℤ (neg-ℤ z)) (left-inverse-law-add-ℤ y)) ∙ - ( left-unit-law-add-ℤ (neg-ℤ z))))) - -distributive-neg-diff-ℤ : - (x y : ℤ) → neg-ℤ (x -ℤ y) ＝ y -ℤ x -distributive-neg-diff-ℤ x y = - ( distributive-neg-add-ℤ x (neg-ℤ y)) ∙ - ( ( ap ((neg-ℤ x) +ℤ_) (neg-neg-ℤ y)) ∙ - ( commutative-add-ℤ (neg-ℤ x) y)) - -interchange-law-add-diff-ℤ : interchange-law add-ℤ diff-ℤ -interchange-law-add-diff-ℤ x y u v = - ( interchange-law-add-add-ℤ x (neg-ℤ y) u (neg-ℤ v)) ∙ - ( ap ((x +ℤ u) +ℤ_) (inv (distributive-neg-add-ℤ y v))) - -interchange-law-diff-add-ℤ : interchange-law diff-ℤ add-ℤ -interchange-law-diff-add-ℤ x y u v = inv (interchange-law-add-diff-ℤ x u y v) - -left-translation-diff-ℤ : - (x y z : ℤ) → (z +ℤ x) -ℤ (z +ℤ y) ＝ x -ℤ y -left-translation-diff-ℤ x y z = - ( interchange-law-diff-add-ℤ z x z y) ∙ - ( ( ap (_+ℤ (x -ℤ y)) (right-inverse-law-add-ℤ z)) ∙ - ( left-unit-law-add-ℤ (x -ℤ y))) - -right-translation-diff-ℤ : - (x y z : ℤ) → (x +ℤ z) -ℤ (y +ℤ z) ＝ x -ℤ y -right-translation-diff-ℤ x y z = - ( ap-diff-ℤ (commutative-add-ℤ x z) (commutative-add-ℤ y z)) ∙ - ( left-translation-diff-ℤ x y z) +```agda +abstract + left-successor-law-diff-ℤ : + (x y : ℤ) → (succ-ℤ x) -ℤ y ＝ succ-ℤ (x -ℤ y) + left-successor-law-diff-ℤ x y = left-successor-law-add-ℤ x (neg-ℤ y) + + right-successor-law-diff-ℤ : + (x y : ℤ) → x -ℤ (succ-ℤ y) ＝ pred-ℤ (x -ℤ y) + right-successor-law-diff-ℤ x y = + ap (x +ℤ_) (neg-succ-ℤ y) ∙ right-predecessor-law-add-ℤ x (neg-ℤ y) + + left-predecessor-law-diff-ℤ : + (x y : ℤ) → (pred-ℤ x) -ℤ y ＝ pred-ℤ (x -ℤ y) + left-predecessor-law-diff-ℤ x y = left-predecessor-law-add-ℤ x (neg-ℤ y) + + right-predecessor-law-diff-ℤ : + (x y : ℤ) → x -ℤ (pred-ℤ y) ＝ succ-ℤ (x -ℤ y) + right-predecessor-law-diff-ℤ x y = + ap (x +ℤ_) (neg-pred-ℤ y) ∙ right-successor-law-add-ℤ x (neg-ℤ y) ``` +### Triangular identity for addition and difference of integers + +```agda +abstract + triangle-diff-ℤ : + (x y z : ℤ) → (x -ℤ y) +ℤ (y -ℤ z) ＝ x -ℤ z + triangle-diff-ℤ x y z = + ( associative-add-ℤ x (neg-ℤ y) (y -ℤ z)) ∙ + ( ap + ( x +ℤ_) + ( ( inv (associative-add-ℤ (neg-ℤ y) y (neg-ℤ z))) ∙ + ( ( ap (_+ℤ (neg-ℤ z)) (left-inverse-law-add-ℤ y)) ∙ + ( left-unit-law-add-ℤ (neg-ℤ z))))) +``` + +### The negative of the difference of two integers `x` and `y` is the difference of `y` and `x` + +```agda +abstract + distributive-neg-diff-ℤ : + (x y : ℤ) → neg-ℤ (x -ℤ y) ＝ y -ℤ x + distributive-neg-diff-ℤ x y = + ( distributive-neg-add-ℤ x (neg-ℤ y)) ∙ + ( ap ((neg-ℤ x) +ℤ_) (neg-neg-ℤ y)) ∙ + ( commutative-add-ℤ (neg-ℤ x) y) +``` + +### Interchange laws for addition and difference of integers + +```agda +abstract + interchange-law-add-diff-ℤ : + (x y u v : ℤ) → (x -ℤ y) +ℤ (u -ℤ v) ＝ (x +ℤ u) -ℤ (y +ℤ v) + interchange-law-add-diff-ℤ x y u v = + ( interchange-law-add-add-ℤ x (neg-ℤ y) u (neg-ℤ v)) ∙ + ( ap ((x +ℤ u) +ℤ_) (inv (distributive-neg-add-ℤ y v))) + + interchange-law-diff-add-ℤ : + (x y u v : ℤ) → (x +ℤ y) -ℤ (u +ℤ v) ＝ (x -ℤ u) +ℤ (y -ℤ v) + interchange-law-diff-add-ℤ x y u v = inv (interchange-law-add-diff-ℤ x u y v) +``` + +### The difference of integers is invariant by translation + +```agda +abstract + left-translation-diff-ℤ : + (x y z : ℤ) → (z +ℤ x) -ℤ (z +ℤ y) ＝ x -ℤ y + left-translation-diff-ℤ x y z = + ( interchange-law-diff-add-ℤ z x z y) ∙ + ( ( ap (_+ℤ (x -ℤ y)) (right-inverse-law-add-ℤ z)) ∙ + ( left-unit-law-add-ℤ (x -ℤ y))) + + right-translation-diff-ℤ : + (x y z : ℤ) → (x +ℤ z) -ℤ (y +ℤ z) ＝ x -ℤ y + right-translation-diff-ℤ x y z = + ( ap-diff-ℤ (commutative-add-ℤ x z) (commutative-add-ℤ y z)) ∙ + ( left-translation-diff-ℤ x y z) +``` + +### The difference of the successors of two integers is their difference + ```agda -diff-succ-ℤ : (x y : ℤ) → (succ-ℤ x) -ℤ (succ-ℤ y) ＝ x -ℤ y -diff-succ-ℤ x y = - ( ap ((succ-ℤ x) +ℤ_) (neg-succ-ℤ y)) ∙ - ( ( left-successor-law-add-ℤ x (pred-ℤ (neg-ℤ y))) ∙ - ( ( ap succ-ℤ (right-predecessor-law-add-ℤ x (neg-ℤ y))) ∙ - ( is-section-pred-ℤ (x -ℤ y)))) +abstract + diff-succ-ℤ : (x y : ℤ) → (succ-ℤ x) -ℤ (succ-ℤ y) ＝ x -ℤ y + diff-succ-ℤ x y = + ( ap ((succ-ℤ x) +ℤ_) (neg-succ-ℤ y)) ∙ + ( left-successor-law-add-ℤ x (pred-ℤ (neg-ℤ y))) ∙ + ( ap succ-ℤ (right-predecessor-law-add-ℤ x (neg-ℤ y))) ∙ + ( is-section-pred-ℤ (x -ℤ y)) ``` diff --git a/src/elementary-number-theory/difference-rational-numbers.lagda.md b/src/elementary-number-theory/difference-rational-numbers.lagda.md new file mode 100644 index 0000000000..7dbe0779c1 --- /dev/null +++ b/src/elementary-number-theory/difference-rational-numbers.lagda.md @@ -0,0 +1,154 @@ +# The difference between rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.difference-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.identity-types +open import foundation.interchange-law +``` + +
+ +## Idea + +The {{#concept "difference" Disambiguation="rational numbers" Agda=diff-ℚ}} of +two [rational numbers](elementary-number-theory.rational-numbers.md) `x` and `y` +is the addition of `x` and the negative of `y`. + +## Definitions + +```agda +diff-ℚ : ℚ → ℚ → ℚ +diff-ℚ x y = x +ℚ (neg-ℚ y) + +infixl 36 _-ℚ_ +_-ℚ_ = diff-ℚ + +ap-diff-ℚ : {x x' y y' : ℚ} → x ＝ x' → y ＝ y' → x -ℚ y ＝ x' -ℚ y' +ap-diff-ℚ p q = ap-binary diff-ℚ p q +``` + +## Properties + +### Two rational numbers with a difference equal to zero are equal + +```agda +abstract + eq-diff-ℚ : {x y : ℚ} → is-zero-ℚ (x -ℚ y) → x ＝ y + eq-diff-ℚ {x} {y} H = + ( inv (right-unit-law-add-ℚ x)) ∙ + ( ap (x +ℚ_) (inv (left-inverse-law-add-ℚ y))) ∙ + ( inv (associative-add-ℚ x (neg-ℚ y) y)) ∙ + ( ap (_+ℚ y) H) ∙ + ( left-unit-law-add-ℚ y) +``` + +### The difference of a rational number with itself is zero + +```agda +abstract + is-zero-diff-ℚ' : (x : ℚ) → is-zero-ℚ (x -ℚ x) + is-zero-diff-ℚ' = right-inverse-law-add-ℚ +``` + +### The difference of two equal rational numbers is zero + +```agda +abstract + is-zero-diff-ℚ : {x y : ℚ} → x ＝ y → is-zero-ℚ (x -ℚ y) + is-zero-diff-ℚ {x} refl = is-zero-diff-ℚ' x +``` + +### The difference of a rational number with zero is itself + +```agda +abstract + right-zero-law-diff-ℚ : (x : ℚ) → x -ℚ zero-ℚ ＝ x + right-zero-law-diff-ℚ = right-unit-law-add-ℚ +``` + +### The difference of zero and a rational number is its negative + +```agda +abstract + left-zero-law-diff-ℚ : (x : ℚ) → zero-ℚ -ℚ x ＝ neg-ℚ x + left-zero-law-diff-ℚ x = left-unit-law-add-ℚ (neg-ℚ x) +``` + +### Triangular identity for addition and difference of rational numbers + +```agda +abstract + triangle-diff-ℚ : + (x y z : ℚ) → (x -ℚ y) +ℚ (y -ℚ z) ＝ x -ℚ z + triangle-diff-ℚ x y z = + ( associative-add-ℚ x (neg-ℚ y) (y -ℚ z)) ∙ + ( ap + ( x +ℚ_) + { neg-ℚ y +ℚ y -ℚ z} + { neg-ℚ z} + ( ( inv (associative-add-ℚ (neg-ℚ y) y (neg-ℚ z))) ∙ + ( ( ap + (_+ℚ (neg-ℚ z)) + { neg-ℚ y +ℚ y} + { zero-ℚ} + ( left-inverse-law-add-ℚ y)) ∙ + ( left-unit-law-add-ℚ (neg-ℚ z))))) +``` + +### The negative of the difference of two rational numbers `x` and `y` is the difference of `y` and `x` + +```agda +abstract + distributive-neg-diff-ℚ : + (x y : ℚ) → neg-ℚ (x -ℚ y) ＝ y -ℚ x + distributive-neg-diff-ℚ x y = + ( distributive-neg-add-ℚ x (neg-ℚ y)) ∙ + ( ap ((neg-ℚ x) +ℚ_) (neg-neg-ℚ y)) ∙ + ( commutative-add-ℚ (neg-ℚ x) y) +``` + +### Interchange laws for addition and difference on rational numbers + +```agda +abstract + interchange-law-diff-add-ℚ : + (x y u v : ℚ) → (x +ℚ y) -ℚ (u +ℚ v) ＝ (x -ℚ u) +ℚ (y -ℚ v) + interchange-law-diff-add-ℚ x y u v = + ( ap ((x +ℚ y) +ℚ_) (distributive-neg-add-ℚ u v)) ∙ + ( interchange-law-add-add-ℚ x y (neg-ℚ u) (neg-ℚ v)) + + interchange-law-add-diff-ℚ : + (x y u v : ℚ) → (x -ℚ y) +ℚ (u -ℚ v) ＝ (x +ℚ u) -ℚ (y +ℚ v) + interchange-law-add-diff-ℚ x y u v = + inv (interchange-law-diff-add-ℚ x u y v) +``` + +### The difference of rational numbers is invariant by translation + +```agda +abstract + left-translation-diff-ℚ : + (x y z : ℚ) → (z +ℚ x) -ℚ (z +ℚ y) ＝ x -ℚ y + left-translation-diff-ℚ x y z = + ( interchange-law-diff-add-ℚ z x z y) ∙ + ( ap (_+ℚ (x -ℚ y)) (right-inverse-law-add-ℚ z)) ∙ + ( left-unit-law-add-ℚ (x -ℚ y)) + + right-translation-diff-ℚ : + (x y z : ℚ) → (x +ℚ z) -ℚ (y +ℚ z) ＝ x -ℚ y + right-translation-diff-ℚ x y z = + ( ap-diff-ℚ (commutative-add-ℚ x z) (commutative-add-ℚ y z)) ∙ + ( left-translation-diff-ℚ x y z) +``` diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md index 8a6883a877..fc8abf413d 100644 --- a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md +++ b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md @@ -59,6 +59,22 @@ gcd-ℤ x y = int-ℕ (nat-gcd-ℤ x y) ## Properties +### The greatest common divisor is invariant under negatives + +```agda +module _ + (x y : ℤ) + where + + preserves-gcd-left-neg-ℤ : gcd-ℤ (neg-ℤ x) y ＝ gcd-ℤ x y + preserves-gcd-left-neg-ℤ = + ap (int-ℕ ∘ (λ z → gcd-ℕ z (abs-ℤ y))) (abs-neg-ℤ x) + + preserves-gcd-right-neg-ℤ : gcd-ℤ x (neg-ℤ y) ＝ gcd-ℤ x y + preserves-gcd-right-neg-ℤ = + ap (int-ℕ ∘ (gcd-ℕ (abs-ℤ x))) (abs-neg-ℤ y) +``` + ### A natural number `d` is a common divisor of two natural numbers `x` and `y` if and only if `int-ℕ d` is a common divisor of `int-ℕ x` and `ind-ℕ y` ```agda diff --git a/src/elementary-number-theory/group-of-rational-numbers.lagda.md b/src/elementary-number-theory/group-of-rational-numbers.lagda.md new file mode 100644 index 0000000000..31db2f6181 --- /dev/null +++ b/src/elementary-number-theory/group-of-rational-numbers.lagda.md @@ -0,0 +1,55 @@ +# The additive group of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.group-of-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.groups +open import group-theory.semigroups +``` + +
+ +## Idea + +The type of [rational numbers](elementary-number-theory.rational-numbers.md) +equipped with [addition](elementary-number-theory.addition-rational-numbers.md) +is a [commutative](group-theory.abelian-groups.md) +[group](group-theory.groups.md) with unit `zero-ℚ` and inverse given by`neg-ℚ`. + +## Definitions + +### The additive abelian group of rational numbers + +```agda +ℚ-Semigroup : Semigroup lzero +pr1 ℚ-Semigroup = ℚ-Set +pr1 (pr2 ℚ-Semigroup) = add-ℚ +pr2 (pr2 ℚ-Semigroup) = associative-add-ℚ + +ℚ-Group : Group lzero +pr1 ℚ-Group = ℚ-Semigroup +pr1 (pr1 (pr2 ℚ-Group)) = zero-ℚ +pr1 (pr2 (pr1 (pr2 ℚ-Group))) = left-unit-law-add-ℚ +pr2 (pr2 (pr1 (pr2 ℚ-Group))) = right-unit-law-add-ℚ +pr1 (pr2 (pr2 ℚ-Group)) = neg-ℚ +pr1 (pr2 (pr2 (pr2 ℚ-Group))) = left-inverse-law-add-ℚ +pr2 (pr2 (pr2 (pr2 ℚ-Group))) = right-inverse-law-add-ℚ + +ℚ-Ab : Ab lzero +pr1 ℚ-Ab = ℚ-Group +pr2 ℚ-Ab = commutative-add-ℚ +``` diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md index 60660edfed..e031c434c7 100644 --- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md @@ -40,7 +40,7 @@ open import foundation.universe-levels ## Idea An [integer fraction](elementary-number-theory.integer-fractions.md) `m/n` is -{{#concept "less or equal" Disambiguation="integer fracion" Agda=leq-fraction-ℤ}} +{{#concept "less or equal" Disambiguation="integer fraction" Agda=leq-fraction-ℤ}} to a fraction `m'/n'` if the [integer product](elementary-number-theory.multiplication-integers.md) `m * n'` is [less or equal](elementary-number-theory.inequality-integers.md) to `m' * n`. diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md index 58ca328611..1e9c9063f6 100644 --- a/src/elementary-number-theory/inequality-integers.lagda.md +++ b/src/elementary-number-theory/inequality-integers.lagda.md @@ -212,6 +212,79 @@ leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H = tr (is-nonnegative-ℤ) ℤ-Poset = (ℤ-Preorder , λ x y → antisymmetric-leq-ℤ) ``` +### An integer `x` is nonnegative if and only if `0 ≤ x` + +```agda +module _ + (x : ℤ) + where + + abstract + leq-zero-is-nonnegative-ℤ : is-nonnegative-ℤ x → leq-ℤ zero-ℤ x + leq-zero-is-nonnegative-ℤ = + is-nonnegative-eq-ℤ (inv (right-zero-law-diff-ℤ x)) + + is-nonnegative-leq-zero-ℤ : leq-ℤ zero-ℤ x → is-nonnegative-ℤ x + is-nonnegative-leq-zero-ℤ = + is-nonnegative-eq-ℤ (right-zero-law-diff-ℤ x) +``` + +### An integer greater than or equal to a nonnegative integer is nonnegative + +```agda +module _ + (x y : ℤ) (I : leq-ℤ x y) + where + + abstract + is-nonnegative-leq-nonnegative-ℤ : is-nonnegative-ℤ x → is-nonnegative-ℤ y + is-nonnegative-leq-nonnegative-ℤ H = + is-nonnegative-leq-zero-ℤ y + ( transitive-leq-ℤ + ( zero-ℤ) + ( x) + ( y) + ( I) + ( leq-zero-is-nonnegative-ℤ x H)) +``` + +### An integer `x` is nonpositive if and only if `x ≤ 0` + +```agda +module _ + (x : ℤ) + where + + abstract + leq-zero-is-nonpositive-ℤ : is-nonpositive-ℤ x → leq-ℤ x zero-ℤ + leq-zero-is-nonpositive-ℤ = is-nonnegative-neg-is-nonpositive-ℤ + + is-nonpositive-leq-zero-ℤ : leq-ℤ x zero-ℤ → is-nonpositive-ℤ x + is-nonpositive-leq-zero-ℤ H = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ x) + ( is-nonpositive-neg-is-nonnegative-ℤ H) +``` + +### An integer less than or equal to a nonpositive integer is nonpositive + +```agda +module _ + (x y : ℤ) (I : leq-ℤ x y) + where + + abstract + is-nonpositive-leq-nonpositive-ℤ : is-nonpositive-ℤ y → is-nonpositive-ℤ x + is-nonpositive-leq-nonpositive-ℤ H = + is-nonpositive-leq-zero-ℤ x + ( transitive-leq-ℤ + ( x) + ( y) + ( zero-ℤ) + ( leq-zero-is-nonpositive-ℤ y H) + ( I)) +``` + ## See also - The decidable total order on the integers is defined in diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index 0919f81e72..c4b8e44389 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -97,7 +97,7 @@ refl-leq-ℚ x = ```agda antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x ＝ y antisymmetric-leq-ℚ x y H H' = - ( inv (in-fraction-fraction-ℚ x)) ∙ + ( inv (is-retraction-rational-fraction-ℚ x)) ∙ ( eq-ℚ-sim-fraction-ℤ ( fraction-ℚ x) ( fraction-ℚ y) @@ -106,7 +106,7 @@ antisymmetric-leq-ℚ x y H H' = ( fraction-ℚ y) ( H) ( H'))) ∙ - ( in-fraction-fraction-ℚ y) + ( is-retraction-rational-fraction-ℚ y) ``` ### Inequality on the rational numbers is linear diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md index 86be352c6c..eacb3714e8 100644 --- a/src/elementary-number-theory/integer-fractions.lagda.md +++ b/src/elementary-number-theory/integer-fractions.lagda.md @@ -67,22 +67,22 @@ is-positive-denominator-fraction-ℤ x = pr2 (positive-denominator-fraction-ℤ ### Inclusion of the integers ```agda -in-fraction-ℤ-ℤ : ℤ → fraction-ℤ -pr1 (in-fraction-ℤ-ℤ x) = x -pr2 (in-fraction-ℤ-ℤ x) = one-positive-ℤ +in-fraction-ℤ : ℤ → fraction-ℤ +pr1 (in-fraction-ℤ x) = x +pr2 (in-fraction-ℤ x) = one-positive-ℤ ``` ### Negative one, zero and one ```agda neg-one-fraction-ℤ : fraction-ℤ -neg-one-fraction-ℤ = in-fraction-ℤ-ℤ neg-one-ℤ +neg-one-fraction-ℤ = in-fraction-ℤ neg-one-ℤ is-neg-one-fraction-ℤ : fraction-ℤ → UU lzero is-neg-one-fraction-ℤ x = (x ＝ neg-one-fraction-ℤ) zero-fraction-ℤ : fraction-ℤ -zero-fraction-ℤ = in-fraction-ℤ-ℤ zero-ℤ +zero-fraction-ℤ = in-fraction-ℤ zero-ℤ is-zero-fraction-ℤ : fraction-ℤ → UU lzero is-zero-fraction-ℤ x = (x ＝ zero-fraction-ℤ) @@ -91,28 +91,37 @@ is-nonzero-fraction-ℤ : fraction-ℤ → UU lzero is-nonzero-fraction-ℤ k = ¬ (is-zero-fraction-ℤ k) one-fraction-ℤ : fraction-ℤ -one-fraction-ℤ = in-fraction-ℤ-ℤ one-ℤ +one-fraction-ℤ = in-fraction-ℤ one-ℤ is-one-fraction-ℤ : fraction-ℤ → UU lzero is-one-fraction-ℤ x = (x ＝ one-fraction-ℤ) ``` +### The negative of an integer fraction + +```agda +neg-fraction-ℤ : fraction-ℤ → fraction-ℤ +neg-fraction-ℤ (d , n) = (neg-ℤ d , n) +``` + ## Properties ### Denominators are nonzero ```agda -is-nonzero-denominator-fraction-ℤ : - (x : fraction-ℤ) → is-nonzero-ℤ (denominator-fraction-ℤ x) -is-nonzero-denominator-fraction-ℤ x = - is-nonzero-is-positive-ℤ (is-positive-denominator-fraction-ℤ x) +abstract + is-nonzero-denominator-fraction-ℤ : + (x : fraction-ℤ) → is-nonzero-ℤ (denominator-fraction-ℤ x) + is-nonzero-denominator-fraction-ℤ x = + is-nonzero-is-positive-ℤ (is-positive-denominator-fraction-ℤ x) ``` ### The type of fractions is a set ```agda -is-set-fraction-ℤ : is-set fraction-ℤ -is-set-fraction-ℤ = is-set-Σ is-set-ℤ λ _ → is-set-positive-ℤ +abstract + is-set-fraction-ℤ : is-set fraction-ℤ + is-set-fraction-ℤ = is-set-Σ is-set-ℤ (λ _ → is-set-positive-ℤ) ``` ```agda @@ -134,55 +143,56 @@ refl-sim-fraction-ℤ x = refl symmetric-sim-fraction-ℤ : is-symmetric sim-fraction-ℤ symmetric-sim-fraction-ℤ x y r = inv r -transitive-sim-fraction-ℤ : is-transitive sim-fraction-ℤ -transitive-sim-fraction-ℤ x y z s r = - is-injective-right-mul-ℤ - ( denominator-fraction-ℤ y) - ( is-nonzero-denominator-fraction-ℤ y) - ( ( associative-mul-ℤ - ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ z) - ( denominator-fraction-ℤ y)) ∙ - ( ap - ( (numerator-fraction-ℤ x) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ z) - ( denominator-fraction-ℤ y))) ∙ - ( inv - ( associative-mul-ℤ +abstract + transitive-sim-fraction-ℤ : is-transitive sim-fraction-ℤ + transitive-sim-fraction-ℤ x y z s r = + is-injective-right-mul-ℤ + ( denominator-fraction-ℤ y) + ( is-nonzero-denominator-fraction-ℤ y) + ( ( associative-mul-ℤ ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ z))) ∙ - ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙ - ( associative-mul-ℤ - ( numerator-fraction-ℤ y) - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ z)) ∙ - ( ap - ( (numerator-fraction-ℤ y) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ z))) ∙ - ( inv + ( denominator-fraction-ℤ z) + ( denominator-fraction-ℤ y)) ∙ + ( ap + ( (numerator-fraction-ℤ x) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ z) + ( denominator-fraction-ℤ y))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ z))) ∙ + ( ap ( _*ℤ (denominator-fraction-ℤ z)) r) ∙ ( associative-mul-ℤ ( numerator-fraction-ℤ y) - ( denominator-fraction-ℤ z) - ( denominator-fraction-ℤ x))) ∙ - ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙ - ( associative-mul-ℤ - ( numerator-fraction-ℤ z) - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ x)) ∙ - ( ap - ( (numerator-fraction-ℤ z) *ℤ_) - ( commutative-mul-ℤ - ( denominator-fraction-ℤ y) - ( denominator-fraction-ℤ x))) ∙ - ( inv + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ z)) ∙ + ( ap + ( (numerator-fraction-ℤ y) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ z))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ z) + ( denominator-fraction-ℤ x))) ∙ + ( ap (_*ℤ (denominator-fraction-ℤ x)) s) ∙ ( associative-mul-ℤ ( numerator-fraction-ℤ z) - ( denominator-fraction-ℤ x) - ( denominator-fraction-ℤ y)))) + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ x)) ∙ + ( ap + ( (numerator-fraction-ℤ z) *ℤ_) + ( commutative-mul-ℤ + ( denominator-fraction-ℤ y) + ( denominator-fraction-ℤ x))) ∙ + ( inv + ( associative-mul-ℤ + ( numerator-fraction-ℤ z) + ( denominator-fraction-ℤ x) + ( denominator-fraction-ℤ y)))) equivalence-relation-sim-fraction-ℤ : equivalence-relation lzero fraction-ℤ pr1 equivalence-relation-sim-fraction-ℤ = sim-fraction-ℤ-Prop @@ -191,21 +201,62 @@ pr1 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = symmetric-sim-fraction- pr2 (pr2 (pr2 equivalence-relation-sim-fraction-ℤ)) = transitive-sim-fraction-ℤ ``` +### The negatives of two similar integer fractions are similar + +```agda +module _ + (x y : fraction-ℤ) + where + + abstract + preserves-sim-neg-fraction-ℤ : + sim-fraction-ℤ x y → sim-fraction-ℤ (neg-fraction-ℤ x) (neg-fraction-ℤ y) + preserves-sim-neg-fraction-ℤ H = + ( left-negative-law-mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y)) ∙ + ( ap neg-ℤ H) ∙ + ( inv + ( left-negative-law-mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ x))) +``` + +### Two integer fractions with zero numerator are similar + +```agda +abstract + sim-is-zero-numerator-fraction-ℤ : + (x y : fraction-ℤ) → + is-zero-ℤ (numerator-fraction-ℤ x) → + is-zero-ℤ (numerator-fraction-ℤ y) → + sim-fraction-ℤ x y + sim-is-zero-numerator-fraction-ℤ x y H K = + eq-is-zero-ℤ + ( ap (_*ℤ (denominator-fraction-ℤ y)) H ∙ + left-zero-law-mul-ℤ (denominator-fraction-ℤ y)) + ( ap (_*ℤ (denominator-fraction-ℤ x)) K ∙ + left-zero-law-mul-ℤ (denominator-fraction-ℤ x)) +``` + ### The greatest common divisor of the numerator and a denominator of a fraction is always a positive integer ```agda -is-positive-gcd-numerator-denominator-fraction-ℤ : - (x : fraction-ℤ) → - is-positive-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) -is-positive-gcd-numerator-denominator-fraction-ℤ x = - is-positive-gcd-is-positive-right-ℤ - ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ x) - ( is-positive-denominator-fraction-ℤ x) - -is-nonzero-gcd-numerator-denominator-fraction-ℤ : - (x : fraction-ℤ) → - is-nonzero-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) -is-nonzero-gcd-numerator-denominator-fraction-ℤ x = - is-nonzero-is-positive-ℤ (is-positive-gcd-numerator-denominator-fraction-ℤ x) +abstract + is-positive-gcd-numerator-denominator-fraction-ℤ : + (x : fraction-ℤ) → + is-positive-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) + is-positive-gcd-numerator-denominator-fraction-ℤ x = + is-positive-gcd-is-positive-right-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ x) + ( is-positive-denominator-fraction-ℤ x) + +abstract + is-nonzero-gcd-numerator-denominator-fraction-ℤ : + (x : fraction-ℤ) → + is-nonzero-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) + is-nonzero-gcd-numerator-denominator-fraction-ℤ x = + is-nonzero-is-positive-ℤ + ( is-positive-gcd-numerator-denominator-fraction-ℤ x) ``` diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md index 47e3948e0f..bc56a2ad9c 100644 --- a/src/elementary-number-theory/integers.lagda.md +++ b/src/elementary-number-theory/integers.lagda.md @@ -54,11 +54,11 @@ negative whole numbers. ### Inclusion of the negative integers ```agda -in-neg : ℕ → ℤ -in-neg n = inl n +in-neg-ℤ : ℕ → ℤ +in-neg-ℤ n = inl n neg-one-ℤ : ℤ -neg-one-ℤ = in-neg zero-ℕ +neg-one-ℤ = in-neg-ℤ zero-ℕ is-neg-one-ℤ : ℤ → UU lzero is-neg-one-ℤ x = (x ＝ neg-one-ℤ) @@ -80,11 +80,11 @@ eq-is-zero-ℤ {a} {b} H K = H ∙ inv K ### Inclusion of the positive integers ```agda -in-pos : ℕ → ℤ -in-pos n = inr (inr n) +in-pos-ℤ : ℕ → ℤ +in-pos-ℤ n = inr (inr n) one-ℤ : ℤ -one-ℤ = in-pos zero-ℕ +one-ℤ = in-pos-ℤ zero-ℕ is-one-ℤ : ℤ → UU lzero is-one-ℤ x = (x ＝ one-ℤ) @@ -95,7 +95,7 @@ is-one-ℤ x = (x ＝ one-ℤ) ```agda int-ℕ : ℕ → ℤ int-ℕ zero-ℕ = zero-ℤ -int-ℕ (succ-ℕ n) = in-pos n +int-ℕ (succ-ℕ n) = in-pos-ℤ n is-injective-int-ℕ : is-injective int-ℕ is-injective-int-ℕ {zero-ℕ} {zero-ℕ} refl = refl @@ -154,8 +154,9 @@ neg-ℤ (inr (inr x)) = inl x ### The type of integers is a set ```agda -is-set-ℤ : is-set ℤ -is-set-ℤ = is-set-coproduct is-set-ℕ (is-set-coproduct is-set-unit is-set-ℕ) +abstract + is-set-ℤ : is-set ℤ + is-set-ℤ = is-set-coproduct is-set-ℕ (is-set-coproduct is-set-unit is-set-ℕ) ℤ-Set : Set lzero pr1 ℤ-Set = ℤ @@ -206,23 +207,25 @@ pr2 equiv-pred-ℤ = is-equiv-pred-ℤ ### The successor function on ℤ is injective and has no fixed points ```agda -is-injective-succ-ℤ : is-injective succ-ℤ -is-injective-succ-ℤ {x} {y} p = - inv (is-retraction-pred-ℤ x) ∙ ap pred-ℤ p ∙ is-retraction-pred-ℤ y - -has-no-fixed-points-succ-ℤ : (x : ℤ) → succ-ℤ x ≠ x -has-no-fixed-points-succ-ℤ (inl zero-ℕ) () -has-no-fixed-points-succ-ℤ (inl (succ-ℕ x)) () -has-no-fixed-points-succ-ℤ (inr (inl star)) () +abstract + is-injective-succ-ℤ : is-injective succ-ℤ + is-injective-succ-ℤ {x} {y} p = + inv (is-retraction-pred-ℤ x) ∙ ap pred-ℤ p ∙ is-retraction-pred-ℤ y + + has-no-fixed-points-succ-ℤ : (x : ℤ) → succ-ℤ x ≠ x + has-no-fixed-points-succ-ℤ (inl zero-ℕ) () + has-no-fixed-points-succ-ℤ (inl (succ-ℕ x)) () + has-no-fixed-points-succ-ℤ (inr (inl star)) () ``` ### The negative function is an involution ```agda -neg-neg-ℤ : neg-ℤ ∘ neg-ℤ ~ id -neg-neg-ℤ (inl n) = refl -neg-neg-ℤ (inr (inl star)) = refl -neg-neg-ℤ (inr (inr n)) = refl +abstract + neg-neg-ℤ : neg-ℤ ∘ neg-ℤ ~ id + neg-neg-ℤ (inl n) = refl + neg-neg-ℤ (inr (inl star)) = refl + neg-neg-ℤ (inr (inr n)) = refl abstract is-equiv-neg-ℤ : is-equiv neg-ℤ @@ -243,46 +246,50 @@ emb-neg-ℤ : ℤ ↪ ℤ pr1 emb-neg-ℤ = neg-ℤ pr2 emb-neg-ℤ = is-emb-neg-ℤ -neg-pred-ℤ : (k : ℤ) → neg-ℤ (pred-ℤ k) ＝ succ-ℤ (neg-ℤ k) -neg-pred-ℤ (inl x) = refl -neg-pred-ℤ (inr (inl star)) = refl -neg-pred-ℤ (inr (inr zero-ℕ)) = refl -neg-pred-ℤ (inr (inr (succ-ℕ x))) = refl - -neg-succ-ℤ : (x : ℤ) → neg-ℤ (succ-ℤ x) ＝ pred-ℤ (neg-ℤ x) -neg-succ-ℤ (inl zero-ℕ) = refl -neg-succ-ℤ (inl (succ-ℕ x)) = refl -neg-succ-ℤ (inr (inl star)) = refl -neg-succ-ℤ (inr (inr x)) = refl - -pred-neg-ℤ : - (k : ℤ) → pred-ℤ (neg-ℤ k) ＝ neg-ℤ (succ-ℤ k) -pred-neg-ℤ (inl zero-ℕ) = refl -pred-neg-ℤ (inl (succ-ℕ x)) = refl -pred-neg-ℤ (inr (inl star)) = refl -pred-neg-ℤ (inr (inr x)) = refl +abstract + neg-pred-ℤ : (k : ℤ) → neg-ℤ (pred-ℤ k) ＝ succ-ℤ (neg-ℤ k) + neg-pred-ℤ (inl x) = refl + neg-pred-ℤ (inr (inl star)) = refl + neg-pred-ℤ (inr (inr zero-ℕ)) = refl + neg-pred-ℤ (inr (inr (succ-ℕ x))) = refl + + neg-succ-ℤ : (x : ℤ) → neg-ℤ (succ-ℤ x) ＝ pred-ℤ (neg-ℤ x) + neg-succ-ℤ (inl zero-ℕ) = refl + neg-succ-ℤ (inl (succ-ℕ x)) = refl + neg-succ-ℤ (inr (inl star)) = refl + neg-succ-ℤ (inr (inr x)) = refl + + pred-neg-ℤ : + (k : ℤ) → pred-ℤ (neg-ℤ k) ＝ neg-ℤ (succ-ℤ k) + pred-neg-ℤ (inl zero-ℕ) = refl + pred-neg-ℤ (inl (succ-ℕ x)) = refl + pred-neg-ℤ (inr (inl star)) = refl + pred-neg-ℤ (inr (inr x)) = refl ``` ### The negative function is injective ```agda -is-injective-neg-ℤ : is-injective neg-ℤ -is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y +abstract + is-injective-neg-ℤ : is-injective neg-ℤ + is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y ``` ### The integer successor of a natural number is the successor of the natural number ```agda -succ-int-ℕ : (x : ℕ) → succ-ℤ (int-ℕ x) ＝ int-ℕ (succ-ℕ x) -succ-int-ℕ zero-ℕ = refl -succ-int-ℕ (succ-ℕ x) = refl +abstract + succ-int-ℕ : (x : ℕ) → succ-ℤ (int-ℕ x) ＝ int-ℕ (succ-ℕ x) + succ-int-ℕ zero-ℕ = refl + succ-int-ℕ (succ-ℕ x) = refl ``` ### An integer is zero if its negative is zero ```agda -is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x -is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl +abstract + is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x + is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl ``` ## See also diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md index 981409d4a8..581cf46b87 100644 --- a/src/elementary-number-theory/modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic.lagda.md @@ -241,7 +241,7 @@ pr1 (equiv-add-ℤ-Mod' k x) = add-ℤ-Mod' k x pr2 (equiv-add-ℤ-Mod' k x) = is-equiv-add-ℤ-Mod' k x is-injective-add-ℤ-Mod : (k : ℕ) (x : ℤ-Mod k) → is-injective (add-ℤ-Mod k x) -is-injective-add-ℤ-Mod zero-ℕ = is-injective-add-ℤ +is-injective-add-ℤ-Mod zero-ℕ = is-injective-left-add-ℤ is-injective-add-ℤ-Mod (succ-ℕ k) = is-injective-add-Fin (succ-ℕ k) is-injective-add-ℤ-Mod' : (k : ℕ) (x : ℤ-Mod k) → is-injective (add-ℤ-Mod' k x) @@ -406,12 +406,12 @@ right-distributive-mul-add-ℤ-Mod (succ-ℕ k) = is-left-mul-neg-one-neg-ℤ-Mod : (k : ℕ) (x : ℤ-Mod k) → neg-ℤ-Mod k x ＝ mul-ℤ-Mod k (neg-one-ℤ-Mod k) x -is-left-mul-neg-one-neg-ℤ-Mod zero-ℕ = is-left-mul-neg-one-neg-ℤ +is-left-mul-neg-one-neg-ℤ-Mod zero-ℕ = inv ∘ left-neg-unit-law-mul-ℤ is-left-mul-neg-one-neg-ℤ-Mod (succ-ℕ k) = is-mul-neg-one-neg-Fin k is-left-mul-neg-one-neg-ℤ-Mod' : (k : ℕ) (x : ℤ-Mod k) → neg-ℤ-Mod k x ＝ mul-ℤ-Mod k x (neg-one-ℤ-Mod k) -is-left-mul-neg-one-neg-ℤ-Mod' zero-ℕ = is-right-mul-neg-one-neg-ℤ +is-left-mul-neg-one-neg-ℤ-Mod' zero-ℕ = inv ∘ right-neg-unit-law-mul-ℤ is-left-mul-neg-one-neg-ℤ-Mod' (succ-ℕ k) = is-mul-neg-one-neg-Fin' k ``` diff --git a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md index 2667c5256a..1a67cfd706 100644 --- a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md +++ b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md @@ -52,7 +52,7 @@ ap-mul-fraction-ℤ p q = ap-binary mul-fraction-ℤ p q ## Properties -### Multiplication respects the similarity relation +### Multiplication on integer fractions respects the similarity relation ```agda sim-fraction-mul-fraction-ℤ : @@ -73,7 +73,7 @@ sim-fraction-mul-fraction-ℤ by interchange-law-mul-mul-ℤ nx' dx ny' dy ``` -### Unit laws +### Unit laws for mulitplication on integer fractions ```agda left-unit-law-mul-fraction-ℤ : @@ -88,7 +88,7 @@ right-unit-law-mul-fraction-ℤ (n , d , p) = ap-mul-ℤ (right-unit-law-mul-ℤ n) (inv (right-unit-law-mul-ℤ d)) ``` -### Multiplication is associative +### Multiplication on integer fractions is associative ```agda associative-mul-fraction-ℤ : @@ -100,7 +100,7 @@ associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz)) ``` -### Multiplication is commutative +### Multiplication on integer fractions is commutative ```agda commutative-mul-fraction-ℤ : diff --git a/src/elementary-number-theory/multiplication-integers.lagda.md b/src/elementary-number-theory/multiplication-integers.lagda.md index 9e2f167eb2..8d9326a47b 100644 --- a/src/elementary-number-theory/multiplication-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-integers.lagda.md @@ -94,7 +94,7 @@ is-plus-or-minus-ℤ x y = (x ＝ y) + (neg-one-ℤ *ℤ x ＝ y) ## Properties -### Laws for multiplication on ℤ +### Multiplication by zero is zero ```agda left-zero-law-mul-ℤ : (k : ℤ) → zero-ℤ *ℤ k ＝ zero-ℤ @@ -108,7 +108,11 @@ right-zero-law-mul-ℤ (inr (inl star)) = refl right-zero-law-mul-ℤ (inr (inr zero-ℕ)) = refl right-zero-law-mul-ℤ (inr (inr (succ-ℕ n))) = right-zero-law-mul-ℤ (inr (inr n)) +``` + +### Unit laws +```agda left-unit-law-mul-ℤ : (k : ℤ) → one-ℤ *ℤ k ＝ k left-unit-law-mul-ℤ k = refl @@ -120,7 +124,11 @@ right-unit-law-mul-ℤ (inr (inl star)) = refl right-unit-law-mul-ℤ (inr (inr zero-ℕ)) = refl right-unit-law-mul-ℤ (inr (inr (succ-ℕ n))) = ap (one-ℤ +ℤ_) (right-unit-law-mul-ℤ (inr (inr n))) +``` + +### Multiplication of an integer by `-1` is equal to the negative +```agda left-neg-unit-law-mul-ℤ : (k : ℤ) → neg-one-ℤ *ℤ k ＝ neg-ℤ k left-neg-unit-law-mul-ℤ k = refl @@ -132,7 +140,11 @@ right-neg-unit-law-mul-ℤ (inr (inl star)) = refl right-neg-unit-law-mul-ℤ (inr (inr zero-ℕ)) = refl right-neg-unit-law-mul-ℤ (inr (inr (succ-ℕ n))) = ap (neg-one-ℤ +ℤ_) (right-neg-unit-law-mul-ℤ (inr (inr n))) +``` + +### Multiplication by the successor or the predecessor of an integer +```agda left-successor-law-mul-ℤ : (k l : ℤ) → (succ-ℤ k) *ℤ l ＝ l +ℤ (k *ℤ l) left-successor-law-mul-ℤ (inl zero-ℕ) l = @@ -157,9 +169,9 @@ left-predecessor-law-mul-ℤ (inr (inr zero-ℕ)) l = inv (left-inverse-law-add-ℤ l) left-predecessor-law-mul-ℤ (inr (inr (succ-ℕ x))) l = ( ap - ( _+ℤ ((in-pos x) *ℤ l)) + ( _+ℤ ((in-pos-ℤ x) *ℤ l)) ( inv (left-inverse-law-add-ℤ l))) ∙ - ( associative-add-ℤ (neg-ℤ l) l ((in-pos x) *ℤ l)) + ( associative-add-ℤ (neg-ℤ l) l ((in-pos-ℤ x) *ℤ l)) right-successor-law-mul-ℤ : (k l : ℤ) → k *ℤ (succ-ℤ l) ＝ k +ℤ (k *ℤ l) @@ -187,16 +199,16 @@ right-successor-law-mul-ℤ (inl (succ-ℕ n)) l = right-successor-law-mul-ℤ (inr (inl star)) l = refl right-successor-law-mul-ℤ (inr (inr zero-ℕ)) l = refl right-successor-law-mul-ℤ (inr (inr (succ-ℕ n))) l = - ( left-successor-law-mul-ℤ (in-pos n) (succ-ℤ l)) ∙ + ( left-successor-law-mul-ℤ (in-pos-ℤ n) (succ-ℤ l)) ∙ ( ( ap ((succ-ℤ l) +ℤ_) (right-successor-law-mul-ℤ (inr (inr n)) l)) ∙ - ( ( inv (associative-add-ℤ (succ-ℤ l) (in-pos n) ((in-pos n) *ℤ l))) ∙ + ( ( inv (associative-add-ℤ (succ-ℤ l) (in-pos-ℤ n) ((in-pos-ℤ n) *ℤ l))) ∙ ( ( ap - ( _+ℤ ((in-pos n) *ℤ l)) - { x = (succ-ℤ l) +ℤ (in-pos n)} - { y = (in-pos (succ-ℕ n)) +ℤ l} - ( ( left-successor-law-add-ℤ l (in-pos n)) ∙ - ( ( ap succ-ℤ (commutative-add-ℤ l (in-pos n))) ∙ - ( inv (left-successor-law-add-ℤ (in-pos n) l))))) ∙ + ( _+ℤ ((in-pos-ℤ n) *ℤ l)) + { x = (succ-ℤ l) +ℤ (in-pos-ℤ n)} + { y = (in-pos-ℤ (succ-ℕ n)) +ℤ l} + ( ( left-successor-law-add-ℤ l (in-pos-ℤ n)) ∙ + ( ( ap succ-ℤ (commutative-add-ℤ l (in-pos-ℤ n))) ∙ + ( inv (left-successor-law-add-ℤ (in-pos-ℤ n) l))))) ∙ ( associative-add-ℤ (inr (inr (succ-ℕ n))) l ((inr (inr n)) *ℤ l))))) right-predecessor-law-mul-ℤ : @@ -208,31 +220,35 @@ right-predecessor-law-mul-ℤ (inl (succ-ℕ n)) l = ( left-predecessor-law-mul-ℤ (inl n) (pred-ℤ l)) ∙ ( ( ap ((neg-ℤ (pred-ℤ l)) +ℤ_) (right-predecessor-law-mul-ℤ (inl n) l)) ∙ ( ( inv - ( associative-add-ℤ (neg-ℤ (pred-ℤ l)) (in-pos n) ((inl n) *ℤ l))) ∙ + ( associative-add-ℤ (neg-ℤ (pred-ℤ l)) (in-pos-ℤ n) ((inl n) *ℤ l))) ∙ ( ( ap ( _+ℤ ((inl n) *ℤ l)) { x = (neg-ℤ (pred-ℤ l)) +ℤ (inr (inr n))} { y = (neg-ℤ (inl (succ-ℕ n))) +ℤ (neg-ℤ l)} - ( ( ap (_+ℤ (in-pos n)) (neg-pred-ℤ l)) ∙ - ( ( left-successor-law-add-ℤ (neg-ℤ l) (in-pos n)) ∙ - ( ( ap succ-ℤ (commutative-add-ℤ (neg-ℤ l) (in-pos n))) ∙ - ( inv (left-successor-law-add-ℤ (in-pos n) (neg-ℤ l))))))) ∙ - ( associative-add-ℤ (in-pos (succ-ℕ n)) (neg-ℤ l) ((inl n) *ℤ l))))) + ( ( ap (_+ℤ (in-pos-ℤ n)) (neg-pred-ℤ l)) ∙ + ( ( left-successor-law-add-ℤ (neg-ℤ l) (in-pos-ℤ n)) ∙ + ( ( ap succ-ℤ (commutative-add-ℤ (neg-ℤ l) (in-pos-ℤ n))) ∙ + ( inv (left-successor-law-add-ℤ (in-pos-ℤ n) (neg-ℤ l))))))) ∙ + ( associative-add-ℤ (in-pos-ℤ (succ-ℕ n)) (neg-ℤ l) ((inl n) *ℤ l))))) right-predecessor-law-mul-ℤ (inr (inl star)) l = refl right-predecessor-law-mul-ℤ (inr (inr zero-ℕ)) l = refl right-predecessor-law-mul-ℤ (inr (inr (succ-ℕ n))) l = - ( left-successor-law-mul-ℤ (in-pos n) (pred-ℤ l)) ∙ + ( left-successor-law-mul-ℤ (in-pos-ℤ n) (pred-ℤ l)) ∙ ( ( ap ((pred-ℤ l) +ℤ_) (right-predecessor-law-mul-ℤ (inr (inr n)) l)) ∙ ( ( inv (associative-add-ℤ (pred-ℤ l) (inl n) ((inr (inr n)) *ℤ l))) ∙ ( ( ap - ( _+ℤ ((in-pos n) *ℤ l)) + ( _+ℤ ((in-pos-ℤ n) *ℤ l)) { x = (pred-ℤ l) +ℤ (inl n)} - { y = (neg-ℤ (in-pos (succ-ℕ n))) +ℤ l} + { y = (neg-ℤ (in-pos-ℤ (succ-ℕ n))) +ℤ l} ( ( left-predecessor-law-add-ℤ l (inl n)) ∙ ( ( ap pred-ℤ (commutative-add-ℤ l (inl n))) ∙ ( inv (left-predecessor-law-add-ℤ (inl n) l))))) ∙ ( associative-add-ℤ (inl (succ-ℕ n)) l ((inr (inr n)) *ℤ l))))) +``` + +### Multiplication on the integers distributes on the right over addition +```agda right-distributive-mul-add-ℤ : (k l m : ℤ) → (k +ℤ l) *ℤ m ＝ (k *ℤ m) +ℤ (l *ℤ m) right-distributive-mul-add-ℤ (inl zero-ℕ) l m = @@ -250,10 +266,14 @@ right-distributive-mul-add-ℤ (inr (inl star)) l m = refl right-distributive-mul-add-ℤ (inr (inr zero-ℕ)) l m = left-successor-law-mul-ℤ l m right-distributive-mul-add-ℤ (inr (inr (succ-ℕ n))) l m = - ( left-successor-law-mul-ℤ ((in-pos n) +ℤ l) m) ∙ + ( left-successor-law-mul-ℤ ((in-pos-ℤ n) +ℤ l) m) ∙ ( ( ap (m +ℤ_) (right-distributive-mul-add-ℤ (inr (inr n)) l m)) ∙ - ( inv (associative-add-ℤ m ((in-pos n) *ℤ m) (l *ℤ m)))) + ( inv (associative-add-ℤ m ((in-pos-ℤ n) *ℤ m) (l *ℤ m)))) +``` + +### Left multiplication by the negative of an integer is the negative of the multiplication +```agda left-negative-law-mul-ℤ : (k l : ℤ) → (neg-ℤ k) *ℤ l ＝ neg-ℤ (k *ℤ l) left-negative-law-mul-ℤ (inl zero-ℕ) l = @@ -269,8 +289,12 @@ left-negative-law-mul-ℤ (inr (inr zero-ℕ)) l = refl left-negative-law-mul-ℤ (inr (inr (succ-ℕ n))) l = ( left-predecessor-law-mul-ℤ (inl n) l) ∙ ( ( ap ((neg-ℤ l) +ℤ_) (left-negative-law-mul-ℤ (inr (inr n)) l)) ∙ - ( inv (distributive-neg-add-ℤ l ((in-pos n) *ℤ l)))) + ( inv (distributive-neg-add-ℤ l ((in-pos-ℤ n) *ℤ l)))) +``` + +### Multiplication on the integers is associative +```agda associative-mul-ℤ : (k l m : ℤ) → (k *ℤ l) *ℤ m ＝ k *ℤ (l *ℤ m) associative-mul-ℤ (inl zero-ℕ) l m = @@ -284,9 +308,13 @@ associative-mul-ℤ (inl (succ-ℕ n)) l m = associative-mul-ℤ (inr (inl star)) l m = refl associative-mul-ℤ (inr (inr zero-ℕ)) l m = refl associative-mul-ℤ (inr (inr (succ-ℕ n))) l m = - ( right-distributive-mul-add-ℤ l ((in-pos n) *ℤ l) m) ∙ + ( right-distributive-mul-add-ℤ l ((in-pos-ℤ n) *ℤ l) m) ∙ ( ap ((l *ℤ m) +ℤ_) (associative-mul-ℤ (inr (inr n)) l m)) +``` + +### Multiplication on the integers is commutative +```agda commutative-mul-ℤ : (k l : ℤ) → k *ℤ l ＝ l *ℤ k commutative-mul-ℤ (inl zero-ℕ) l = inv (right-neg-unit-law-mul-ℤ l) @@ -297,36 +325,34 @@ commutative-mul-ℤ (inr (inl star)) l = inv (right-zero-law-mul-ℤ l) commutative-mul-ℤ (inr (inr zero-ℕ)) l = inv (right-unit-law-mul-ℤ l) commutative-mul-ℤ (inr (inr (succ-ℕ n))) l = ( ap (l +ℤ_) (commutative-mul-ℤ (inr (inr n)) l)) ∙ - ( inv (right-successor-law-mul-ℤ l (in-pos n))) + ( inv (right-successor-law-mul-ℤ l (in-pos-ℤ n))) +``` + +### Multiplication on the integers distributes on the left over addition +```agda left-distributive-mul-add-ℤ : (m k l : ℤ) → m *ℤ (k +ℤ l) ＝ (m *ℤ k) +ℤ (m *ℤ l) left-distributive-mul-add-ℤ m k l = commutative-mul-ℤ m (k +ℤ l) ∙ ( ( right-distributive-mul-add-ℤ k l m) ∙ ( ap-add-ℤ (commutative-mul-ℤ k m) (commutative-mul-ℤ l m))) +``` + +### Right multiplication by the negative of an integer is the negative of the multiplication +```agda right-negative-law-mul-ℤ : (k l : ℤ) → k *ℤ (neg-ℤ l) ＝ neg-ℤ (k *ℤ l) right-negative-law-mul-ℤ k l = ( ( commutative-mul-ℤ k (neg-ℤ l)) ∙ ( left-negative-law-mul-ℤ l k)) ∙ ( ap neg-ℤ (commutative-mul-ℤ l k)) +``` -interchange-law-mul-mul-ℤ : interchange-law mul-ℤ mul-ℤ -interchange-law-mul-mul-ℤ = - interchange-law-commutative-and-associative - mul-ℤ - commutative-mul-ℤ - associative-mul-ℤ - -is-left-mul-neg-one-neg-ℤ : (x : ℤ) → neg-ℤ x ＝ neg-one-ℤ *ℤ x -is-left-mul-neg-one-neg-ℤ x = refl - -is-right-mul-neg-one-neg-ℤ : (x : ℤ) → neg-ℤ x ＝ x *ℤ neg-one-ℤ -is-right-mul-neg-one-neg-ℤ x = - is-left-mul-neg-one-neg-ℤ x ∙ commutative-mul-ℤ neg-one-ℤ x +### The multiplication of the negatives of two integers is equal to their multiplication +```agda double-negative-law-mul-ℤ : (k l : ℤ) → (neg-ℤ k) *ℤ (neg-ℤ l) ＝ k *ℤ l double-negative-law-mul-ℤ k l = equational-reasoning @@ -339,6 +365,18 @@ double-negative-law-mul-ℤ k l = by neg-neg-ℤ (k *ℤ l) ``` +### Interchange law + +```agda +interchange-law-mul-mul-ℤ : + (x y u v : ℤ) → (x *ℤ y) *ℤ (u *ℤ v) ＝ (x *ℤ u) *ℤ (y *ℤ v) +interchange-law-mul-mul-ℤ = + interchange-law-commutative-and-associative + mul-ℤ + commutative-mul-ℤ + associative-mul-ℤ +``` + ### Computing multiplication of integers that come from natural numbers ```agda @@ -407,22 +445,24 @@ compute-mul-ℤ (inr (inr (succ-ℕ x))) (inr (inr y)) = ( ap int-ℕ (commutative-add-ℕ (succ-ℕ y) ((succ-ℕ x) *ℕ (succ-ℕ y))))) ``` -### Linearity of the difference +### Multiplication on integers distributes over the difference ```agda -linear-diff-left-mul-ℤ : - (z x y : ℤ) → (z *ℤ x) -ℤ (z *ℤ y) ＝ z *ℤ (x -ℤ y) -linear-diff-left-mul-ℤ z x y = - ( ap ((z *ℤ x) +ℤ_) (inv (right-negative-law-mul-ℤ z y))) ∙ - ( inv (left-distributive-mul-add-ℤ z x (neg-ℤ y))) - -linear-diff-right-mul-ℤ : - (x y z : ℤ) → (x *ℤ z) -ℤ (y *ℤ z) ＝ (x -ℤ y) *ℤ z -linear-diff-right-mul-ℤ x y z = - ( ap ((x *ℤ z) +ℤ_) (inv (left-negative-law-mul-ℤ y z))) ∙ - ( inv (right-distributive-mul-add-ℤ x (neg-ℤ y) z)) +left-distributive-mul-diff-ℤ : + (z x y : ℤ) → z *ℤ (x -ℤ y) ＝ (z *ℤ x) -ℤ (z *ℤ y) +left-distributive-mul-diff-ℤ z x y = + ( left-distributive-mul-add-ℤ z x (neg-ℤ y)) ∙ + ( ap ((z *ℤ x) +ℤ_) (right-negative-law-mul-ℤ z y)) + +right-distributive-mul-diff-ℤ : + (x y z : ℤ) → (x -ℤ y) *ℤ z ＝ (x *ℤ z) -ℤ (y *ℤ z) +right-distributive-mul-diff-ℤ x y z = + ( right-distributive-mul-add-ℤ x (neg-ℤ y) z) ∙ + ( ap ((x *ℤ z) +ℤ_) (left-negative-law-mul-ℤ y z)) ``` +### If the product of two integers is zero, one of the factors is zero + ```agda is-zero-is-zero-mul-ℤ : (x y : ℤ) → is-zero-ℤ (x *ℤ y) → (is-zero-ℤ x) + (is-zero-ℤ y) @@ -439,7 +479,7 @@ is-zero-is-zero-mul-ℤ (inr (inr x)) (inr (inr y)) H = ex-falso (Eq-eq-ℤ (inv (compute-mul-ℤ (inr (inr x)) (inr (inr y))) ∙ H)) ``` -### Injectivity of multiplication +### Injectivity of multiplication by a nonzero integer ```agda is-injective-left-mul-ℤ : @@ -452,7 +492,7 @@ is-injective-left-mul-ℤ x f {y} {z} p = ( f) ( is-zero-is-zero-mul-ℤ x ( y -ℤ z) - ( inv (linear-diff-left-mul-ℤ x y z) ∙ is-zero-diff-ℤ p))) + ( left-distributive-mul-diff-ℤ x y z ∙ is-zero-diff-ℤ p))) is-injective-right-mul-ℤ : (x : ℤ) → is-nonzero-ℤ x → is-injective (_*ℤ x) diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md index ed5eaf8aa0..a8c0e801c0 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md @@ -336,21 +336,21 @@ int-mul-nonpositive-ℤ' x y = y *ℤ int-nonpositive-ℤ x ```agda mul-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ -mul-positive-ℤ (x , H) (y , K) = mul-ℤ x y , is-positive-mul-ℤ H K +mul-positive-ℤ (x , H) (y , K) = (mul-ℤ x y , is-positive-mul-ℤ H K) ``` ### Multiplication of nonnegative integers ```agda mul-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ → nonnegative-ℤ -mul-nonnegative-ℤ (x , H) (y , K) = mul-ℤ x y , is-nonnegative-mul-ℤ H K +mul-nonnegative-ℤ (x , H) (y , K) = (mul-ℤ x y , is-nonnegative-mul-ℤ H K) ``` ### Multiplication of negative integers ```agda mul-negative-ℤ : negative-ℤ → negative-ℤ → positive-ℤ -mul-negative-ℤ (x , H) (y , K) = mul-ℤ x y , is-positive-mul-negative-ℤ H K +mul-negative-ℤ (x , H) (y , K) = (mul-ℤ x y , is-positive-mul-negative-ℤ H K) ``` ### Multiplication of nonpositive integers @@ -358,7 +358,7 @@ mul-negative-ℤ (x , H) (y , K) = mul-ℤ x y , is-positive-mul-negative-ℤ H ```agda mul-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ → nonnegative-ℤ mul-nonpositive-ℤ (x , H) (y , K) = - mul-ℤ x y , is-nonnegative-mul-nonpositive-ℤ H K + (mul-ℤ x y , is-nonnegative-mul-nonpositive-ℤ H K) ``` ## Properties @@ -374,14 +374,14 @@ module _ le-ℤ x y → le-ℤ (int-mul-positive-ℤ z x) (int-mul-positive-ℤ z y) preserves-le-right-mul-positive-ℤ K = is-positive-eq-ℤ - ( inv (linear-diff-left-mul-ℤ (int-positive-ℤ z) y x)) + ( left-distributive-mul-diff-ℤ (int-positive-ℤ z) y x) ( is-positive-mul-ℤ (is-positive-int-positive-ℤ z) K) preserves-le-left-mul-positive-ℤ : le-ℤ x y → le-ℤ (int-mul-positive-ℤ' z x) (int-mul-positive-ℤ' z y) preserves-le-left-mul-positive-ℤ K = is-positive-eq-ℤ - ( inv (linear-diff-right-mul-ℤ y x (int-positive-ℤ z))) + ( right-distributive-mul-diff-ℤ y x (int-positive-ℤ z)) ( is-positive-mul-ℤ K (is-positive-int-positive-ℤ z)) reflects-le-right-mul-positive-ℤ : @@ -389,7 +389,7 @@ module _ reflects-le-right-mul-positive-ℤ K = is-positive-right-factor-mul-ℤ ( is-positive-eq-ℤ - ( linear-diff-left-mul-ℤ (int-positive-ℤ z) y x) + ( inv (left-distributive-mul-diff-ℤ (int-positive-ℤ z) y x)) ( K)) ( is-positive-int-positive-ℤ z) @@ -398,7 +398,7 @@ module _ reflects-le-left-mul-positive-ℤ K = is-positive-left-factor-mul-ℤ ( is-positive-eq-ℤ - ( linear-diff-right-mul-ℤ y x (int-positive-ℤ z)) + ( inv (right-distributive-mul-diff-ℤ y x (int-positive-ℤ z))) ( K)) ( is-positive-int-positive-ℤ z) ``` @@ -414,13 +414,13 @@ module _ leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ z x) (int-mul-nonnegative-ℤ z y) preserves-leq-right-mul-nonnegative-ℤ K = is-nonnegative-eq-ℤ - ( inv (linear-diff-left-mul-ℤ (int-nonnegative-ℤ z) y x)) + ( left-distributive-mul-diff-ℤ (int-nonnegative-ℤ z) y x) ( is-nonnegative-mul-ℤ (is-nonnegative-int-nonnegative-ℤ z) K) preserves-leq-left-mul-nonnegative-ℤ : leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ' z x) (int-mul-nonnegative-ℤ' z y) preserves-leq-left-mul-nonnegative-ℤ K = is-nonnegative-eq-ℤ - ( inv (linear-diff-right-mul-ℤ y x (int-nonnegative-ℤ z))) + ( right-distributive-mul-diff-ℤ y x (int-nonnegative-ℤ z)) ( is-nonnegative-mul-ℤ K (is-nonnegative-int-nonnegative-ℤ z)) ``` diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md index f220975b16..30cb40c66f 100644 --- a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md @@ -9,12 +9,22 @@ module elementary-number-theory.multiplication-rational-numbers where
Imports ```agda +open import elementary-number-theory.addition-integer-fractions +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integer-fractions +open import elementary-number-theory.multiplication-integers open import elementary-number-theory.rational-numbers +open import elementary-number-theory.reduced-integer-fractions +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types open import foundation.dependent-pair-types +open import foundation.function-types open import foundation.identity-types +open import foundation.interchange-law ```
@@ -32,7 +42,7 @@ rational numbers. ```agda mul-ℚ : ℚ → ℚ → ℚ -mul-ℚ (x , p) (y , q) = in-fraction-ℤ (mul-fraction-ℤ x y) +mul-ℚ (x , p) (y , q) = rational-fraction-ℤ (mul-fraction-ℤ x y) infixl 40 _*ℚ_ _*ℚ_ = mul-ℚ @@ -40,7 +50,7 @@ _*ℚ_ = mul-ℚ ## Properties -### Unit laws +### Unit laws for multiplication on rational numbers ```agda left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x @@ -49,7 +59,7 @@ left-unit-law-mul-ℚ x = ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x)) ( fraction-ℚ x) ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ - ( in-fraction-fraction-ℚ x) + ( is-retraction-rational-fraction-ℚ x) right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x right-unit-law-mul-ℚ x = @@ -57,5 +67,116 @@ right-unit-law-mul-ℚ x = ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ) ( fraction-ℚ x) ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ - ( in-fraction-fraction-ℚ x) + ( is-retraction-rational-fraction-ℚ x) +``` + +### Multiplication of a rational number by `-1` is equal to the negative + +```agda +left-neg-unit-law-mul-ℚ : (x : ℚ) → neg-one-ℚ *ℚ x ＝ neg-ℚ x +left-neg-unit-law-mul-ℚ x = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ neg-one-ℚ) (fraction-ℚ x)) + ( neg-fraction-ℤ (fraction-ℚ x)) + ( ap-mul-ℤ + ( left-neg-unit-law-mul-ℤ (numerator-ℚ x)) + ( inv (left-unit-law-mul-ℤ (denominator-ℚ x))))) ∙ + ( is-retraction-rational-fraction-ℚ (neg-ℚ x)) + +right-neg-unit-law-mul-ℚ : (x : ℚ) → x *ℚ neg-one-ℚ ＝ neg-ℚ x +right-neg-unit-law-mul-ℚ x = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ neg-one-ℚ)) + ( neg-fraction-ℤ (fraction-ℚ x)) + ( ap-mul-ℤ + ( right-neg-unit-law-mul-ℤ (numerator-ℚ x)) + ( inv (right-unit-law-mul-ℤ (denominator-ℚ x))))) ∙ + ( is-retraction-rational-fraction-ℚ (neg-ℚ x)) +``` + +### Multiplication of rational numbers is associative + +```agda +associative-mul-ℚ : + (x y z : ℚ) → (x *ℚ y) *ℚ z ＝ x *ℚ (y *ℚ z) +associative-mul-ℚ x y z = + eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ z)) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z))) + ( transitive-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ z)) + ( mul-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( fraction-ℚ z)) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z))) + ( transitive-sim-fraction-ℤ + ( mul-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( fraction-ℚ z)) + ( mul-fraction-ℤ + ( fraction-ℚ x) + ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y *ℚ z))) + ( sim-fraction-mul-fraction-ℤ + ( refl-sim-fraction-ℤ (fraction-ℚ x)) + ( sim-reduced-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))) + ( associative-mul-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z))) + ( sim-fraction-mul-fraction-ℤ + ( inv + ( sim-reduced-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))) + ( refl-sim-fraction-ℤ (fraction-ℚ z)))) +``` + +### Multiplication of rational numbers is commutative + +```agda +commutative-mul-ℚ : (x y : ℚ) → x *ℚ y ＝ y *ℚ x +commutative-mul-ℚ x y = + eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( mul-fraction-ℤ (fraction-ℚ y) (fraction-ℚ x)) + ( commutative-mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) +``` + +### Interchange law for multiplication on rational numbers with itself + +```agda +interchange-law-mul-mul-ℚ : + (x y u v : ℚ) → (x *ℚ y) *ℚ (u *ℚ v) ＝ (x *ℚ u) *ℚ (y *ℚ v) +interchange-law-mul-mul-ℚ = + interchange-law-commutative-and-associative + mul-ℚ + commutative-mul-ℚ + associative-mul-ℚ +``` + +### Negative laws for multiplication on rational numbers + +```agda +module _ + (x y : ℚ) + where + + left-negative-law-mul-ℚ : (neg-ℚ x) *ℚ y ＝ neg-ℚ (x *ℚ y) + left-negative-law-mul-ℚ = + ( ap ( _*ℚ y) (inv (left-neg-unit-law-mul-ℚ x))) ∙ + ( associative-mul-ℚ neg-one-ℚ x y) ∙ + ( left-neg-unit-law-mul-ℚ (x *ℚ y)) + + right-negative-law-mul-ℚ : x *ℚ (neg-ℚ y) ＝ neg-ℚ (x *ℚ y) + right-negative-law-mul-ℚ = + ( ap ( x *ℚ_) (inv (right-neg-unit-law-mul-ℚ y))) ∙ + ( inv (associative-mul-ℚ x y neg-one-ℚ)) ∙ + ( right-neg-unit-law-mul-ℚ (x *ℚ y)) + +negative-law-mul-ℚ : (x y : ℚ) → (neg-ℚ x) *ℚ (neg-ℚ y) ＝ x *ℚ y +negative-law-mul-ℚ x y = + ( left-negative-law-mul-ℚ x (neg-ℚ y)) ∙ + ( ap neg-ℚ (right-negative-law-mul-ℚ x y)) ∙ + ( neg-neg-ℚ (x *ℚ y)) ``` diff --git a/src/elementary-number-theory/negative-integers.lagda.md b/src/elementary-number-theory/negative-integers.lagda.md index e99dfc6a58..a549a3ae37 100644 --- a/src/elementary-number-theory/negative-integers.lagda.md +++ b/src/elementary-number-theory/negative-integers.lagda.md @@ -9,6 +9,7 @@ module elementary-number-theory.negative-integers where ```agda open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -106,6 +107,13 @@ decidable-subtype-negative-ℤ x = is-decidable-is-negative-ℤ x) ``` +### Negative integers are nonzero + +```agda +is-nonzero-is-negative-ℤ : {x : ℤ} → is-negative-ℤ x → is-nonzero-ℤ x +is-nonzero-is-negative-ℤ {inl x} H () +``` + ### The negative integers form a set ```agda diff --git a/src/elementary-number-theory/nonzero-integers.lagda.md b/src/elementary-number-theory/nonzero-integers.lagda.md index 1c9fac8416..d5b2dcd318 100644 --- a/src/elementary-number-theory/nonzero-integers.lagda.md +++ b/src/elementary-number-theory/nonzero-integers.lagda.md @@ -83,3 +83,10 @@ pr2 one-nonzero-ℤ = is-nonzero-one-ℤ is-nonzero-int-ℕ : (n : ℕ) → is-nonzero-ℕ n → is-nonzero-ℤ (int-ℕ n) is-nonzero-int-ℕ zero-ℕ H p = H refl ``` + +### The negative of a nonzero integer is nonzero + +```agda +is-nonzero-neg-nonzero-ℤ : (x : ℤ) → is-nonzero-ℤ x → is-nonzero-ℤ (neg-ℤ x) +is-nonzero-neg-nonzero-ℤ x H K = H (is-zero-is-zero-neg-ℤ x K) +``` diff --git a/src/elementary-number-theory/positive-and-negative-integers.lagda.md b/src/elementary-number-theory/positive-and-negative-integers.lagda.md index 82a5630d33..844b95a8b8 100644 --- a/src/elementary-number-theory/positive-and-negative-integers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-integers.lagda.md @@ -15,6 +15,7 @@ open import elementary-number-theory.nonpositive-integers open import elementary-number-theory.nonzero-integers open import elementary-number-theory.positive-integers +open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types @@ -42,18 +43,12 @@ is-zero-is-nonnegative-is-nonpositive-ℤ : is-zero-is-nonnegative-is-nonpositive-ℤ {inr (inl x)} H K = refl ``` -### Positive integers are nonzero +### No integer is both positive and negative ```agda -is-nonzero-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonzero-ℤ x -is-nonzero-is-positive-ℤ {inr (inr x)} H () -``` - -### Negative integers are nonzero - -```agda -is-nonzero-is-negative-ℤ : {x : ℤ} → is-negative-ℤ x → is-nonzero-ℤ x -is-nonzero-is-negative-ℤ {inl x} H () +is-not-negative-and-positive-ℤ : (x : ℤ) → ¬ (is-negative-ℤ x × is-positive-ℤ x) +is-not-negative-and-positive-ℤ (inl x) (H , K) = K +is-not-negative-and-positive-ℤ (inr x) (H , K) = H ``` ### Dichotomies diff --git a/src/elementary-number-theory/positive-integers.lagda.md b/src/elementary-number-theory/positive-integers.lagda.md index 1732ac0bc6..5b25d4a0e2 100644 --- a/src/elementary-number-theory/positive-integers.lagda.md +++ b/src/elementary-number-theory/positive-integers.lagda.md @@ -9,6 +9,7 @@ module elementary-number-theory.positive-integers where ```agda open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -108,6 +109,13 @@ decidable-subtype-positive-ℤ x = is-decidable-is-positive-ℤ x) ``` +### Positive integers are nonzero + +```agda +is-nonzero-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonzero-ℤ x +is-nonzero-is-positive-ℤ {inr (inr x)} H () +``` + ### The positive integers form a set ```agda diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index cd01f83dcf..0e730f26eb 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -12,10 +12,12 @@ open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.mediant-integer-fractions +open import elementary-number-theory.multiplication-integers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integers open import elementary-number-theory.reduced-integer-fractions +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.equality-dependent-pair-types @@ -69,29 +71,31 @@ module _ ### Inclusion of fractions ```agda -in-fraction-ℤ : fraction-ℤ → ℚ -pr1 (in-fraction-ℤ x) = reduce-fraction-ℤ x -pr2 (in-fraction-ℤ x) = is-reduced-reduce-fraction-ℤ x +rational-fraction-ℤ : fraction-ℤ → ℚ +pr1 (rational-fraction-ℤ x) = reduce-fraction-ℤ x +pr2 (rational-fraction-ℤ x) = is-reduced-reduce-fraction-ℤ x ``` ### Inclusion of the integers ```agda -in-int : ℤ → ℚ -in-int x = pair (pair x one-positive-ℤ) (is-one-gcd-one-ℤ' x) +rational-ℤ : ℤ → ℚ +pr1 (pr1 (rational-ℤ x)) = x +pr2 (pr1 (rational-ℤ x)) = one-positive-ℤ +pr2 (rational-ℤ x) = is-one-gcd-one-ℤ' x ``` ### Negative one, zero and one ```agda neg-one-ℚ : ℚ -neg-one-ℚ = in-int neg-one-ℤ +neg-one-ℚ = rational-ℤ neg-one-ℤ is-neg-one-ℚ : ℚ → UU lzero is-neg-one-ℚ x = (x ＝ neg-one-ℚ) zero-ℚ : ℚ -zero-ℚ = in-int zero-ℤ +zero-ℚ = rational-ℤ zero-ℤ is-zero-ℚ : ℚ → UU lzero is-zero-ℚ x = (x ＝ zero-ℚ) @@ -100,18 +104,26 @@ is-nonzero-ℚ : ℚ → UU lzero is-nonzero-ℚ k = ¬ (is-zero-ℚ k) one-ℚ : ℚ -one-ℚ = in-int one-ℤ +one-ℚ = rational-ℤ one-ℤ is-one-ℚ : ℚ → UU lzero is-one-ℚ x = (x ＝ one-ℚ) ``` +### The negative of a rational number + +```agda +neg-ℚ : ℚ → ℚ +pr1 (neg-ℚ (x , H)) = neg-fraction-ℤ x +pr2 (neg-ℚ (x , H)) = is-reduced-neg-fraction-ℤ x H +``` + ### The mediant of two rationals ```agda mediant-ℚ : ℚ → ℚ → ℚ mediant-ℚ x y = - in-fraction-ℤ + rational-fraction-ℤ ( mediant-fraction-ℤ ( fraction-ℚ x) ( fraction-ℚ y)) @@ -124,7 +136,7 @@ mediant-ℚ x y = ```agda eq-ℚ-sim-fraction-ℤ : (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) → - in-fraction-ℤ x ＝ in-fraction-ℤ y + rational-fraction-ℤ x ＝ rational-fraction-ℤ y eq-ℚ-sim-fraction-ℤ x y H = eq-pair-Σ' ( pair @@ -135,32 +147,116 @@ eq-ℚ-sim-fraction-ℤ x y H = ### The type of rationals is a set ```agda -is-set-ℚ : is-set ℚ -is-set-ℚ = - is-set-Σ - ( is-set-fraction-ℤ) - ( λ x → is-set-is-prop (is-prop-is-reduced-fraction-ℤ x)) +abstract + is-set-ℚ : is-set ℚ + is-set-ℚ = + is-set-Σ + ( is-set-fraction-ℤ) + ( λ x → is-set-is-prop (is-prop-is-reduced-fraction-ℤ x)) ℚ-Set : Set lzero pr1 ℚ-Set = ℚ pr2 ℚ-Set = is-set-ℚ -in-fraction-fraction-ℚ : (x : ℚ) → in-fraction-ℤ (fraction-ℚ x) ＝ x -in-fraction-fraction-ℚ (pair (pair m (pair n n-pos)) p) = - eq-pair-Σ - ( eq-pair - ( eq-quotient-div-is-one-ℤ _ _ p (div-left-gcd-ℤ m n)) - ( eq-pair-Σ - ( eq-quotient-div-is-one-ℤ _ _ p (div-right-gcd-ℤ m n)) - ( eq-is-prop (is-prop-is-positive-ℤ n)))) - ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (m , n , n-pos))) +abstract + is-retraction-rational-fraction-ℚ : + (x : ℚ) → rational-fraction-ℤ (fraction-ℚ x) ＝ x + is-retraction-rational-fraction-ℚ (pair (pair m (pair n n-pos)) p) = + eq-pair-Σ + ( eq-pair + ( eq-quotient-div-is-one-ℤ _ _ p (div-left-gcd-ℤ m n)) + ( eq-pair-Σ + ( eq-quotient-div-is-one-ℤ _ _ p (div-right-gcd-ℤ m n)) + ( eq-is-prop (is-prop-is-positive-ℤ n)))) + ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (m , n , n-pos))) +``` + +### Two fractions with the same numerator and same denominator are equal + +```agda +module _ + ( x y : ℚ) + ( H : numerator-ℚ x ＝ numerator-ℚ y) + ( K : denominator-ℚ x ＝ denominator-ℚ y) + where + + abstract + eq-ℚ : x ＝ y + eq-ℚ = + ( inv (is-retraction-rational-fraction-ℚ x)) ∙ + ( eq-ℚ-sim-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( ap-mul-ℤ H (inv K))) ∙ + ( is-retraction-rational-fraction-ℚ y) +``` + +### A rational number is zero if and only if its numerator is zero + +```agda +module _ + (x : ℚ) + where + + abstract + is-zero-numerator-is-zero-ℚ : + is-zero-ℚ x → is-zero-ℤ (numerator-ℚ x) + is-zero-numerator-is-zero-ℚ = ap numerator-ℚ + + is-zero-is-zero-numerator-ℚ : + is-zero-ℤ (numerator-ℚ x) → is-zero-ℚ x + is-zero-is-zero-numerator-ℚ H = + ( inv (is-retraction-rational-fraction-ℚ x)) ∙ + ( eq-ℚ-sim-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ zero-ℚ) + ( eq-is-zero-ℤ + ( ap (mul-ℤ' one-ℤ) H ∙ right-zero-law-mul-ℤ one-ℤ) + ( left-zero-law-mul-ℤ (denominator-ℚ x)))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) +``` + +### The rational image of the negative of an integer is the rational negative of its image + +```agda +abstract + preserves-neg-rational-ℤ : + (k : ℤ) → rational-ℤ (neg-ℤ k) ＝ neg-ℚ (rational-ℤ k) + preserves-neg-rational-ℤ k = + eq-ℚ (rational-ℤ (neg-ℤ k)) (neg-ℚ (rational-ℤ k)) refl refl +``` + +### The reduced fraction of the negative of an integer fraction is the negative of the reduced fraction + +```agda +abstract + preserves-neg-rational-fraction-ℤ : + (x : fraction-ℤ) → + rational-fraction-ℤ (neg-fraction-ℤ x) ＝ neg-ℚ (rational-fraction-ℤ x) + preserves-neg-rational-fraction-ℤ x = + ( eq-ℚ-sim-fraction-ℤ + ( neg-fraction-ℤ x) + ( fraction-ℚ (neg-ℚ (rational-fraction-ℤ x))) + ( preserves-sim-neg-fraction-ℤ + ( x) + ( reduce-fraction-ℤ x) + ( sim-reduced-fraction-ℤ x))) ∙ + ( is-retraction-rational-fraction-ℚ (neg-ℚ (rational-fraction-ℤ x))) +``` + +### The negative function on the rational numbers is an involution + +```agda +abstract + neg-neg-ℚ : (x : ℚ) → neg-ℚ (neg-ℚ x) ＝ x + neg-neg-ℚ x = eq-ℚ (neg-ℚ (neg-ℚ x)) x (neg-neg-ℤ (numerator-ℚ x)) refl ``` -### The reflecting map from ℤ to ℚ +### The reflecting map from `fraction-ℤ` to `ℚ` ```agda reflecting-map-sim-fraction : reflecting-map-equivalence-relation equivalence-relation-sim-fraction-ℤ ℚ -pr1 reflecting-map-sim-fraction = in-fraction-ℤ +pr1 reflecting-map-sim-fraction = rational-fraction-ℤ pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fraction-ℤ x y H ``` diff --git a/src/elementary-number-theory/reduced-integer-fractions.lagda.md b/src/elementary-number-theory/reduced-integer-fractions.lagda.md index 291af5d0c0..b74d316dd3 100644 --- a/src/elementary-number-theory/reduced-integer-fractions.lagda.md +++ b/src/elementary-number-theory/reduced-integer-fractions.lagda.md @@ -64,6 +64,22 @@ is-prop-is-reduced-fraction-ℤ x = ( denominator-fraction-ℤ x) ``` +### The negative of a reduced integer fraction is reduced + +```agda +is-reduced-neg-fraction-ℤ : + (x : fraction-ℤ) → + is-reduced-fraction-ℤ x → + is-reduced-fraction-ℤ (neg-fraction-ℤ x) +is-reduced-neg-fraction-ℤ x = + tr + ( is-one-ℤ) + ( inv + ( preserves-gcd-left-neg-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ x))) +``` + ### Any fraction can be reduced ```agda diff --git a/src/elementary-number-theory/ring-of-integers.lagda.md b/src/elementary-number-theory/ring-of-integers.lagda.md index a775c913c0..1ef3b8fff6 100644 --- a/src/elementary-number-theory/ring-of-integers.lagda.md +++ b/src/elementary-number-theory/ring-of-integers.lagda.md @@ -14,6 +14,7 @@ open import elementary-number-theory.group-of-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -28,6 +29,7 @@ open import ring-theory.homomorphisms-rings open import ring-theory.initial-rings open import ring-theory.integer-multiples-of-elements-rings open import ring-theory.rings +open import ring-theory.trivial-rings ``` @@ -52,6 +54,13 @@ pr2 ℤ-Commutative-Ring = commutative-mul-ℤ ## Properties +### The ring of integers is nontrivial + +```agda +is-nontrivial-ℤ-Ring : is-nontrivial-Ring ℤ-Ring +is-nontrivial-ℤ-Ring H = is-nonzero-one-ℤ (inv H) +``` + ### The integer multiples in `ℤ-Ring` coincide with multiplication in `ℤ` ```agda @@ -59,7 +68,7 @@ is-mul-integer-multiple-ℤ-Ring : (k l : ℤ) → integer-multiple-Ring ℤ-Ring k l ＝ mul-ℤ k l is-mul-integer-multiple-ℤ-Ring (inl zero-ℕ) l = ( integer-multiple-neg-one-Ring ℤ-Ring l) ∙ - ( is-left-mul-neg-one-neg-ℤ l) + ( inv (left-neg-unit-law-mul-ℤ l)) is-mul-integer-multiple-ℤ-Ring (inl (succ-ℕ k)) l = ( integer-multiple-pred-Ring ℤ-Ring (inl k) l) ∙ ( ap diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index c943654ab8..0801560c95 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -226,6 +226,20 @@ module _ ( is-positive-denominator-fraction-ℤ q) ``` +### The similarity of integer fractions preserves strict inequality + +```agda +module _ + (p q p' q' : fraction-ℤ) (H : sim-fraction-ℤ p p') (K : sim-fraction-ℤ q q') + where + + preserves-le-sim-fraction-ℤ : le-fraction-ℤ p q → le-fraction-ℤ p' q' + preserves-le-sim-fraction-ℤ I = + concatenate-sim-le-fraction-ℤ p' p q' + ( symmetric-sim-fraction-ℤ p p' H) + ( concatenate-le-sim-fraction-ℤ p q q' I K) +``` + ### Fractions with equal denominator compare the same as their numerators ```agda diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 20bc5040ac..c371c4e803 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -179,3 +179,74 @@ reflects-le-right-add-ℤ : reflects-le-right-add-ℤ z x y = is-positive-eq-ℤ (left-translation-diff-ℤ y x z) ``` + +### An integer `x` is positive if and only if `0 < x` + +```agda +module _ + (x : ℤ) + where + + abstract + le-zero-is-positive-ℤ : is-positive-ℤ x → le-ℤ zero-ℤ x + le-zero-is-positive-ℤ = is-positive-eq-ℤ (inv (right-zero-law-diff-ℤ x)) + + is-positive-le-zero-ℤ : le-ℤ zero-ℤ x → is-positive-ℤ x + is-positive-le-zero-ℤ = is-positive-eq-ℤ (right-zero-law-diff-ℤ x) +``` + +### If an integer is greater than a positive integer it is positive + +```agda +module _ + (x y : ℤ) (I : le-ℤ x y) + where + + abstract + is-positive-le-positive-ℤ : is-positive-ℤ x → is-positive-ℤ y + is-positive-le-positive-ℤ H = + is-positive-le-zero-ℤ y + ( transitive-le-ℤ + ( zero-ℤ) + ( x) + ( y) + ( I) + ( le-zero-is-positive-ℤ x H)) +``` + +### An integer `x` is negative if and only if `x < 0` + +```agda +module _ + (x : ℤ) + where + + abstract + le-zero-is-negative-ℤ : is-negative-ℤ x → le-ℤ x zero-ℤ + le-zero-is-negative-ℤ = is-positive-neg-is-negative-ℤ + + is-negative-le-zero-ℤ : le-ℤ x zero-ℤ → is-negative-ℤ x + is-negative-le-zero-ℤ H = + is-negative-eq-ℤ + ( neg-neg-ℤ x) + ( is-negative-neg-is-positive-ℤ H) +``` + +### If an integer is lesser than a negative integer it is negative + +```agda +module _ + (x y : ℤ) (I : le-ℤ x y) + where + + abstract + is-negative-le-negative-ℤ : is-negative-ℤ y → is-negative-ℤ x + is-negative-le-negative-ℤ H = + is-negative-le-zero-ℤ x + ( transitive-le-ℤ + ( x) + ( y) + ( zero-ℤ) + ( le-zero-is-negative-ℤ y H) + ( I)) +``` diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index 6bbdc58319..0f342d811e 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -145,35 +145,48 @@ module _ ( fraction-ℚ z) ``` -### Strict inequality on the rational numbers reflects the strict inequality of their underlying fractions +### The canonical map from integer fractions to the rational numbers preserves strict inequality ```agda +module _ + (p q : fraction-ℤ) + where + + preserves-le-rational-fraction-ℤ : + le-fraction-ℤ p q → le-ℚ (rational-fraction-ℤ p) (rational-fraction-ℤ q) + preserves-le-rational-fraction-ℤ = + preserves-le-sim-fraction-ℤ + ( p) + ( q) + ( reduce-fraction-ℤ p) + ( reduce-fraction-ℤ q) + ( sim-reduced-fraction-ℤ p) + ( sim-reduced-fraction-ℤ q) + module _ (x : ℚ) (p : fraction-ℤ) where - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : - le-fraction-ℤ (fraction-ℚ x) p → - le-ℚ x (in-fraction-ℤ p) - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H = + preserves-le-right-rational-fraction-ℤ : + le-fraction-ℤ (fraction-ℚ x) p → le-ℚ x (rational-fraction-ℤ p) + preserves-le-right-rational-fraction-ℤ H = concatenate-le-sim-fraction-ℤ ( fraction-ℚ x) ( p) - ( fraction-ℚ ( in-fraction-ℤ p)) + ( fraction-ℚ ( rational-fraction-ℤ p)) ( H) ( sim-reduced-fraction-ℤ p) - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : - le-fraction-ℤ p (fraction-ℚ x) → - le-ℚ (in-fraction-ℤ p) x - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ = + preserves-le-left-rational-fraction-ℤ : + le-fraction-ℤ p (fraction-ℚ x) → le-ℚ (rational-fraction-ℤ p) x + preserves-le-left-rational-fraction-ℤ = concatenate-sim-le-fraction-ℤ - ( fraction-ℚ ( in-fraction-ℤ p)) + ( fraction-ℚ ( rational-fraction-ℤ p)) ( p) ( fraction-ℚ x) ( symmetric-sim-fraction-ℤ ( p) - ( fraction-ℚ ( in-fraction-ℤ p)) + ( fraction-ℚ ( rational-fraction-ℤ p)) ( sim-reduced-fraction-ℤ p)) ``` @@ -186,8 +199,8 @@ module _ left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x) left-∃-le-ℚ = intro-∃ - ( in-fraction-ℤ frac) - ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( rational-fraction-ℤ frac) + ( preserves-le-left-rational-fraction-ℤ x frac ( le-fraction-le-numerator-fraction-ℤ ( frac) ( fraction-ℚ x) @@ -199,8 +212,8 @@ module _ right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r) right-∃-le-ℚ = intro-∃ - ( in-fraction-ℤ frac) - ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( rational-fraction-ℤ frac) + ( preserves-le-right-rational-fraction-ℤ x frac ( le-fraction-le-numerator-fraction-ℤ ( fraction-ℚ x) ( frac) @@ -251,13 +264,13 @@ module _ le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y) le-left-mediant-ℚ = - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x + preserves-le-right-rational-fraction-ℤ x ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y le-right-mediant-ℚ = - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y + preserves-le-left-rational-fraction-ℤ y ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) ``` diff --git a/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md b/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md index 3f55ca21ca..e592961eb4 100644 --- a/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/integer-multiples-of-elements-abelian-groups.lagda.md @@ -118,14 +118,14 @@ module _ integer-multiple-in-pos-Ab : (n : ℕ) (a : type-Ab A) → - integer-multiple-Ab A (in-pos n) a ＝ + integer-multiple-Ab A (in-pos-ℤ n) a ＝ multiple-Ab A (succ-ℕ n) a integer-multiple-in-pos-Ab = integer-power-in-pos-Group (group-Ab A) integer-multiple-in-neg-Ab : (n : ℕ) (a : type-Ab A) → - integer-multiple-Ab A (in-neg n) a ＝ + integer-multiple-Ab A (in-neg-ℤ n) a ＝ neg-Ab A (multiple-Ab A (succ-ℕ n) a) integer-multiple-in-neg-Ab = integer-power-in-neg-Group (group-Ab A) diff --git a/src/group-theory/integer-powers-of-elements-groups.lagda.md b/src/group-theory/integer-powers-of-elements-groups.lagda.md index e934125857..1e105e8922 100644 --- a/src/group-theory/integer-powers-of-elements-groups.lagda.md +++ b/src/group-theory/integer-powers-of-elements-groups.lagda.md @@ -159,13 +159,13 @@ module _ integer-power-in-pos-Group : (n : ℕ) (g : type-Group G) → - integer-power-Group G (in-pos n) g ＝ + integer-power-Group G (in-pos-ℤ n) g ＝ power-Group G (succ-ℕ n) g integer-power-in-pos-Group n g = integer-power-int-Group (succ-ℕ n) g integer-power-in-neg-Group : (n : ℕ) (g : type-Group G) → - integer-power-Group G (in-neg n) g ＝ + integer-power-Group G (in-neg-ℤ n) g ＝ inv-Group G (power-Group G (succ-ℕ n) g) integer-power-in-neg-Group zero-ℕ g = right-unit-law-mul-Group G (inv-Group G g) @@ -489,23 +489,23 @@ module _ ( integer-power-one-Group G y))) distributive-integer-power-mul-Group (inr (inr (succ-ℕ k))) x y H = equational-reasoning - (x * y) ^ (succ-ℤ (in-pos k)) - ＝ (x * y) ^ (in-pos k) * (x * y) - by integer-power-succ-Group G (in-pos k) (x * y) - ＝ (x ^ (in-pos k) * y ^ (in-pos k)) * (x * y) + (x * y) ^ (succ-ℤ (in-pos-ℤ k)) + ＝ (x * y) ^ (in-pos-ℤ k) * (x * y) + by integer-power-succ-Group G (in-pos-ℤ k) (x * y) + ＝ (x ^ (in-pos-ℤ k) * y ^ (in-pos-ℤ k)) * (x * y) by ap ( _* (x * y)) ( distributive-integer-power-mul-Group (inr (inr k)) x y H) - ＝ (x ^ (in-pos k) * x) * (y ^ (in-pos k) * y) + ＝ (x ^ (in-pos-ℤ k) * x) * (y ^ (in-pos-ℤ k) * y) by interchange-mul-mul-Group G - ( inv (commute-integer-powers-Group' G (in-pos k) H)) - ＝ x ^ (succ-ℤ (in-pos k)) * y ^ (succ-ℤ (in-pos k)) + ( inv (commute-integer-powers-Group' G (in-pos-ℤ k) H)) + ＝ x ^ (succ-ℤ (in-pos-ℤ k)) * y ^ (succ-ℤ (in-pos-ℤ k)) by ap-mul-Group G - ( inv (integer-power-succ-Group G (in-pos k) x)) - ( inv (integer-power-succ-Group G (in-pos k) y)) + ( inv (integer-power-succ-Group G (in-pos-ℤ k) x)) + ( inv (integer-power-succ-Group G (in-pos-ℤ k) y)) ``` ### Powers by products of integers are iterated integer powers @@ -557,18 +557,18 @@ module _ ( inv (integer-power-one-Group G _)) integer-power-mul-Group k (inr (inr (succ-ℕ l))) x = equational-reasoning - (x ^ (k * succ-ℤ (in-pos l))) - ＝ x ^ (k +ℤ k * (in-pos l)) - by ap (x ^_) (right-successor-law-mul-ℤ k (in-pos l)) - ＝ mul-Group G (x ^ k) (x ^ (k * in-pos l)) + (x ^ (k * succ-ℤ (in-pos-ℤ l))) + ＝ x ^ (k +ℤ k * (in-pos-ℤ l)) + by ap (x ^_) (right-successor-law-mul-ℤ k (in-pos-ℤ l)) + ＝ mul-Group G (x ^ k) (x ^ (k * in-pos-ℤ l)) by - distributive-integer-power-add-Group G x k (k * in-pos l) - ＝ mul-Group G (x ^ k) ((x ^ k) ^ (in-pos l)) + distributive-integer-power-add-Group G x k (k * in-pos-ℤ l) + ＝ mul-Group G (x ^ k) ((x ^ k) ^ (in-pos-ℤ l)) by ap (mul-Group G _) (integer-power-mul-Group k (inr (inr l)) x) - ＝ (x ^ k) ^ (succ-ℤ (in-pos l)) + ＝ (x ^ k) ^ (succ-ℤ (in-pos-ℤ l)) by - inv (integer-power-succ-Group' G (in-pos l) (x ^ k)) + inv (integer-power-succ-Group' G (in-pos-ℤ l) (x ^ k)) swap-integer-power-Group : (k l : ℤ) (x : type-Group G) → diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index b76bbfaf7b..eb34a051e8 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -93,8 +93,8 @@ is-dedekind-cut-le-ℚ x = ### The canonical map from `ℚ` to `ℝ` ```agda -real-rational : ℚ → ℝ lzero -real-rational x = +real-ℚ : ℚ → ℝ lzero +real-ℚ x = real-dedekind-cut ( λ (q : ℚ) → le-ℚ-Prop q x) ( λ (r : ℚ) → le-ℚ-Prop x r) @@ -186,18 +186,18 @@ module _ ### The real embedding of a rational number is rational ```agda -is-rational-real-rational : (p : ℚ) → is-rational-ℝ (real-rational p) p -is-rational-real-rational p = irreflexive-le-ℚ p , irreflexive-le-ℚ p +is-rational-real-ℚ : (p : ℚ) → is-rational-ℝ (real-ℚ p) p +is-rational-real-ℚ p = (irreflexive-le-ℚ p , irreflexive-le-ℚ p) ``` ### Rational real numbers are embedded rationals ```agda eq-real-rational-is-rational-ℝ : - (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-rational q ＝ x + (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-ℚ q ＝ x eq-real-rational-is-rational-ℝ x q H = eq-eq-lower-cut-ℝ - ( real-rational q) + ( real-ℚ q) ( x) ( eq-has-same-elements-subtype ( λ p → le-ℚ-Prop p q) @@ -219,25 +219,25 @@ eq-real-rational-is-rational-ℝ x q H = ### The cannonical map from rationals to rational reals ```agda -rational-ℝ-rational : ℚ → Rational-ℝ lzero -rational-ℝ-rational q = real-rational q , q , is-rational-real-rational q +rational-real-ℚ : ℚ → Rational-ℝ lzero +rational-real-ℚ q = (real-ℚ q , q , is-rational-real-ℚ q) ``` ### The rationals and rational reals are equivalent ```agda -is-section-rational-ℝ-rational : +is-section-rational-real-ℚ : (q : ℚ) → - rational-rational-ℝ (rational-ℝ-rational q) ＝ q -is-section-rational-ℝ-rational q = refl + rational-rational-ℝ (rational-real-ℚ q) ＝ q +is-section-rational-real-ℚ q = refl -is-retraction-rational-ℝ-rational : +is-retraction-rational-real-ℚ : (x : Rational-ℝ lzero) → - rational-ℝ-rational (rational-rational-ℝ x) ＝ x -is-retraction-rational-ℝ-rational (x , q , H) = + rational-real-ℚ (rational-rational-ℝ x) ＝ x +is-retraction-rational-real-ℚ (x , q , H) = eq-type-subtype subtype-rational-real - ( ap real-rational α ∙ eq-real-rational-is-rational-ℝ x q H) + ( ap real-ℚ α ∙ eq-real-rational-is-rational-ℝ x q H) where α : rational-rational-ℝ (x , q , H) ＝ q α = refl @@ -249,9 +249,9 @@ pr2 equiv-rational-real = where section-rational-rational-ℝ : section rational-rational-ℝ section-rational-rational-ℝ = - rational-ℝ-rational , is-section-rational-ℝ-rational + (rational-real-ℚ , is-section-rational-real-ℚ) retraction-rational-rational-ℝ : retraction rational-rational-ℝ retraction-rational-rational-ℝ = - rational-ℝ-rational , is-retraction-rational-ℝ-rational + (rational-real-ℚ , is-retraction-rational-real-ℚ) ``` diff --git a/src/ring-theory/integer-multiples-of-elements-rings.lagda.md b/src/ring-theory/integer-multiples-of-elements-rings.lagda.md index 9533254260..9f66654609 100644 --- a/src/ring-theory/integer-multiples-of-elements-rings.lagda.md +++ b/src/ring-theory/integer-multiples-of-elements-rings.lagda.md @@ -122,14 +122,14 @@ module _ integer-multiple-in-pos-Ring : (n : ℕ) (a : type-Ring R) → - integer-multiple-Ring R (in-pos n) a ＝ + integer-multiple-Ring R (in-pos-ℤ n) a ＝ multiple-Ring R (succ-ℕ n) a integer-multiple-in-pos-Ring = integer-multiple-in-pos-Ab (ab-Ring R) integer-multiple-in-neg-Ring : (n : ℕ) (a : type-Ring R) → - integer-multiple-Ring R (in-neg n) a ＝ + integer-multiple-Ring R (in-neg-ℤ n) a ＝ neg-Ring R (multiple-Ring R (succ-ℕ n) a) integer-multiple-in-neg-Ring = integer-multiple-in-neg-Ab (ab-Ring R)