From e62e35effbef4901850734475f482cbcc8e12e60 Mon Sep 17 00:00:00 2001 From: malarbol Date: Wed, 10 Apr 2024 03:41:45 +0200 Subject: [PATCH 1/8] ring of rational numbers --- src/elementary-number-theory.lagda.md | 1 + .../multiplication-integer-fractions.lagda.md | 39 +++++ .../multiplication-rational-numbers.lagda.md | 133 ++++++++++++++++++ .../ring-of-rational-numbers.lagda.md | 56 ++++++++ 4 files changed, 229 insertions(+) create mode 100644 src/elementary-number-theory/ring-of-rational-numbers.lagda.md diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 58a4cc7ffa..881d5328d7 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -123,6 +123,7 @@ open import elementary-number-theory.relatively-prime-natural-numbers public open import elementary-number-theory.repeating-element-standard-finite-type public open import elementary-number-theory.retracts-of-natural-numbers public open import elementary-number-theory.ring-of-integers public +open import elementary-number-theory.ring-of-rational-numbers public open import elementary-number-theory.sieve-of-eratosthenes public open import elementary-number-theory.square-free-natural-numbers public open import elementary-number-theory.squares-integers public diff --git a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md index 1a67cfd706..bd04ae4826 100644 --- a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md +++ b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md @@ -7,11 +7,15 @@ module elementary-number-theory.multiplication-integer-fractions where
Imports ```agda +open import elementary-number-theory.addition-integer-fractions +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 ``` @@ -108,3 +112,38 @@ commutative-mul-fraction-ℤ : commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx) ``` + +### Multiplication on integer fractions distributes on the left over addition + +```agda +left-distributive-mul-add-fraction-ℤ : + (x y z : fraction-ℤ) → + sim-fraction-ℤ + (mul-fraction-ℤ x (add-fraction-ℤ y z)) + (add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z)) +left-distributive-mul-add-fraction-ℤ + (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = + ( ap + ( ( nx *ℤ (ny *ℤ dz +ℤ nz *ℤ dy)) *ℤ_) + ( ( interchange-law-mul-mul-ℤ dx dy dx dz) ∙ + ( associative-mul-ℤ dx dx (dy *ℤ dz)))) ∙ + ( interchange-law-mul-mul-ℤ + ( nx) + ( ny *ℤ dz +ℤ nz *ℤ dy) + ( dx) + ( dx *ℤ (dy *ℤ dz))) ∙ + ( inv + ( associative-mul-ℤ + ( nx *ℤ dx) + ( ny *ℤ dz +ℤ nz *ℤ dy) + ( dx *ℤ (dy *ℤ dz)))) ∙ + ( ap + ( _*ℤ (dx *ℤ (dy *ℤ dz))) + ( ( left-distributive-mul-add-ℤ + ( nx *ℤ dx) + ( ny *ℤ dz) + ( nz *ℤ dy)) ∙ + ( ap-add-ℤ + ( interchange-law-mul-mul-ℤ nx dx ny dz)) + ( interchange-law-mul-mul-ℤ nx dx nz dy))) +``` diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md index 30cb40c66f..fdb9982d6f 100644 --- a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md @@ -11,6 +11,7 @@ module elementary-number-theory.multiplication-rational-numbers where ```agda open import elementary-number-theory.addition-integer-fractions open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers @@ -44,12 +45,70 @@ rational numbers. mul-ℚ : ℚ → ℚ → ℚ mul-ℚ (x , p) (y , q) = rational-fraction-ℤ (mul-fraction-ℤ x y) +mul-ℚ' : ℚ → ℚ → ℚ +mul-ℚ' x y = mul-ℚ y x + infixl 40 _*ℚ_ _*ℚ_ = mul-ℚ ``` ## Properties +### The multiplication of a rational number by zero is zero + +```agda +module _ + (x : ℚ) + where + + left-zero-law-mul-ℚ : zero-ℚ *ℚ x ＝ zero-ℚ + left-zero-law-mul-ℚ = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ zero-ℚ) (fraction-ℚ x)) + ( fraction-ℚ zero-ℚ) + ( eq-is-zero-ℤ + ( ap (mul-ℤ' one-ℤ) (left-zero-law-mul-ℤ (numerator-ℚ x))) + ( left-zero-law-mul-ℤ _))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) + + right-zero-law-mul-ℚ : x *ℚ zero-ℚ ＝ zero-ℚ + right-zero-law-mul-ℚ = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ zero-ℚ)) + ( fraction-ℚ zero-ℚ) + ( eq-is-zero-ℤ + ( ap (mul-ℤ' one-ℤ) (right-zero-law-mul-ℤ (numerator-ℚ x))) + ( left-zero-law-mul-ℤ _))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) +``` + +### If the product of two rational numbers is zero, the left or right factor is zero + +```agda +is-zero-is-zero-mul-ℚ : + (x y : ℚ) → is-zero-ℚ (x *ℚ y) → (is-zero-ℚ x) + (is-zero-ℚ y) +is-zero-is-zero-mul-ℚ x y H = + rec-coproduct + ( inl ∘ is-zero-is-zero-numerator-ℚ x) + ( inr ∘ is-zero-is-zero-numerator-ℚ y) + ( is-zero-is-zero-mul-ℤ + ( numerator-ℚ x) + ( numerator-ℚ y) + ( ( inv + ( eq-reduce-numerator-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)))) ∙ + ( ap + ( mul-ℤ' + ( gcd-ℤ + ( numerator-ℚ x *ℤ numerator-ℚ y) + ( denominator-ℚ x *ℤ denominator-ℚ y))) + ( ( is-zero-numerator-is-zero-ℚ (x *ℚ y) H) ∙ + ( left-zero-law-mul-ℤ + ( gcd-ℤ + (numerator-ℚ x *ℤ numerator-ℚ y) + (denominator-ℚ x *ℤ denominator-ℚ y))))))) +``` + ### Unit laws for multiplication on rational numbers ```agda @@ -179,4 +238,78 @@ negative-law-mul-ℚ x y = ( left-negative-law-mul-ℚ x (neg-ℚ y)) ∙ ( ap neg-ℚ (right-negative-law-mul-ℚ x y)) ∙ ( neg-neg-ℚ (x *ℚ y)) + +swap-neg-mul-ℚ : (x y : ℚ) → x *ℚ (neg-ℚ y) ＝ (neg-ℚ x) *ℚ y +swap-neg-mul-ℚ x y = + ( right-negative-law-mul-ℚ x y) ∙ + ( inv (left-negative-law-mul-ℚ x y)) +``` + +### Multiplication on rational numbers distributes over addition + +```agda +left-distributive-mul-add-ℚ : + (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ x *ℚ y +ℚ x *ℚ z +left-distributive-mul-add-ℚ x y z = + eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) + ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) + ( transitive-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) + ( mul-fraction-ℤ + ( fraction-ℚ x) + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) + ( transitive-sim-fraction-ℤ + ( mul-fraction-ℤ + ( fraction-ℚ x) + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( add-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z))) + ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) + ( sim-fraction-add-fraction-ℤ + ( sim-reduced-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))) + ( sim-reduced-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z)))) + ( left-distributive-mul-add-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z))) + ( sim-fraction-mul-fraction-ℤ + ( refl-sim-fraction-ℤ (fraction-ℚ x)) + ( transitive-sim-fraction-ℤ + ( fraction-ℚ (y +ℚ z)) + ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) + ( symmetric-sim-fraction-ℤ + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) + ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( sim-reduced-fraction-ℤ + (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))) + ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z)))))) + +right-distributive-mul-add-ℚ : + (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ x *ℚ z +ℚ y *ℚ z +right-distributive-mul-add-ℚ x y z = + ( commutative-mul-ℚ (x +ℚ y) z) ∙ + ( left-distributive-mul-add-ℚ z x y) ∙ + ( ap-add-ℚ (commutative-mul-ℚ z x) (commutative-mul-ℚ z y)) +``` + +### Multiplication on rational numbers distributes over the difference + +```agda +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)) ``` diff --git a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md new file mode 100644 index 0000000000..3dbf7593f9 --- /dev/null +++ b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md @@ -0,0 +1,56 @@ +# The ring of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.ring-of-rational-numbers where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-rings + +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.group-of-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.universe-levels + +open import ring-theory.rings +``` + +
+ +## Idea + +The +[commutative group of rational numbers](elementary-number-theory.group-of-rational-numbers.md) +equipped with +[multiplication](elementary-number-theory.multiplication-rational-numbers.md) is +a [commutative](commutative-algebra.commutative-rings.md) +[ring](ring-theory.rings.md). + +## Definitions + +### The commutative ring of rational numbers + +```agda +ℚ-Ring : Ring lzero +pr1 ℚ-Ring = ℚ-Ab +pr1 (pr1 (pr2 ℚ-Ring)) = mul-ℚ +pr2 (pr1 (pr2 ℚ-Ring)) = associative-mul-ℚ +pr1 (pr1 (pr2 (pr2 ℚ-Ring))) = one-ℚ +pr1 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = left-unit-law-mul-ℚ +pr2 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = right-unit-law-mul-ℚ +pr1 (pr2 (pr2 (pr2 ℚ-Ring))) = left-distributive-mul-add-ℚ +pr2 (pr2 (pr2 (pr2 ℚ-Ring))) = right-distributive-mul-add-ℚ + +ℚ-Commutative-Ring : Commutative-Ring lzero +pr1 ℚ-Commutative-Ring = ℚ-Ring +pr2 ℚ-Commutative-Ring = commutative-mul-ℚ +``` From 9aafc960fd75375df5270633b86be98139b17032 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 01:21:13 +0200 Subject: [PATCH 2/8] apply review suggestions --- .../multiplication-rational-numbers.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md index fdb9982d6f..383d71a3d5 100644 --- a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md @@ -85,9 +85,9 @@ module _ ### If the product of two rational numbers is zero, the left or right factor is zero ```agda -is-zero-is-zero-mul-ℚ : +decide-is-zero-factor-is-zero-mul-ℚ : (x y : ℚ) → is-zero-ℚ (x *ℚ y) → (is-zero-ℚ x) + (is-zero-ℚ y) -is-zero-is-zero-mul-ℚ x y H = +decide-is-zero-factor-is-zero-mul-ℚ x y H = rec-coproduct ( inl ∘ is-zero-is-zero-numerator-ℚ x) ( inr ∘ is-zero-is-zero-numerator-ℚ y) @@ -249,7 +249,7 @@ swap-neg-mul-ℚ x y = ```agda left-distributive-mul-add-ℚ : - (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ x *ℚ y +ℚ x *ℚ z + (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ (x *ℚ y) +ℚ (x *ℚ z) left-distributive-mul-add-ℚ x y z = eq-ℚ-sim-fraction-ℤ ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) @@ -291,7 +291,7 @@ left-distributive-mul-add-ℚ x y z = ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z)))))) right-distributive-mul-add-ℚ : - (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ x *ℚ z +ℚ y *ℚ z + (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ (x *ℚ z) +ℚ (y *ℚ z) right-distributive-mul-add-ℚ x y z = ( commutative-mul-ℚ (x +ℚ y) z) ∙ ( left-distributive-mul-add-ℚ z x y) ∙ From 18d3e4046c29b960b2df494c981ffcf51bd7846c Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 02:35:26 +0200 Subject: [PATCH 3/8] refactor ring properties --- .../ring-of-rational-numbers.lagda.md | 32 +++++++++++++++---- 1 file changed, 25 insertions(+), 7 deletions(-) diff --git a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md index 3dbf7593f9..d55eb180ed 100644 --- a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md @@ -19,8 +19,11 @@ open import elementary-number-theory.rational-numbers open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types +open import foundation.unital-binary-operations open import foundation.universe-levels +open import group-theory.semigroups + open import ring-theory.rings ``` @@ -35,6 +38,27 @@ equipped with a [commutative](commutative-algebra.commutative-rings.md) [ring](ring-theory.rings.md). +## Lemmas + +### The abelian group of rational numbers has a compatible multiplicative structure + +```agda +has-associative-mul-ℚ : has-associative-mul ℚ +pr1 has-associative-mul-ℚ = mul-ℚ +pr2 has-associative-mul-ℚ = associative-mul-ℚ + +is-unital-mul-ℚ : is-unital mul-ℚ +pr1 is-unital-mul-ℚ = one-ℚ +pr1 (pr2 is-unital-mul-ℚ) = left-unit-law-mul-ℚ +pr2 (pr2 is-unital-mul-ℚ) = right-unit-law-mul-ℚ + +has-mul-Ab-ℚ : has-mul-Ab ℚ-Ab +pr1 has-mul-Ab-ℚ = has-associative-mul-ℚ +pr1 (pr2 has-mul-Ab-ℚ) = is-unital-mul-ℚ +pr1 (pr2 (pr2 has-mul-Ab-ℚ)) = left-distributive-mul-add-ℚ +pr2 (pr2 (pr2 has-mul-Ab-ℚ)) = right-distributive-mul-add-ℚ +``` + ## Definitions ### The commutative ring of rational numbers @@ -42,13 +66,7 @@ a [commutative](commutative-algebra.commutative-rings.md) ```agda ℚ-Ring : Ring lzero pr1 ℚ-Ring = ℚ-Ab -pr1 (pr1 (pr2 ℚ-Ring)) = mul-ℚ -pr2 (pr1 (pr2 ℚ-Ring)) = associative-mul-ℚ -pr1 (pr1 (pr2 (pr2 ℚ-Ring))) = one-ℚ -pr1 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = left-unit-law-mul-ℚ -pr2 (pr2 (pr1 (pr2 (pr2 ℚ-Ring)))) = right-unit-law-mul-ℚ -pr1 (pr2 (pr2 (pr2 ℚ-Ring))) = left-distributive-mul-add-ℚ -pr2 (pr2 (pr2 (pr2 ℚ-Ring))) = right-distributive-mul-add-ℚ +pr2 ℚ-Ring = has-mul-Ab-ℚ ℚ-Commutative-Ring : Commutative-Ring lzero pr1 ℚ-Commutative-Ring = ℚ-Ring From 41121d5f582addb5d9a31355d985eb8c4e44aa44 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 16:39:32 +0200 Subject: [PATCH 4/8] fix link --- src/elementary-number-theory/addition-rational-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md index 54ded78bf8..9a2824ceb8 100644 --- a/src/elementary-number-theory/addition-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md @@ -162,4 +162,4 @@ abstract ## See also - The additive group structure on the rational numbers is defined in - [elementary-number-theory.group-of-rational-numbers.md]. + [`elementary-number-theory.group-of-rational-numbers`](elementary-number-theory.group-of-rational-numbers.md). From c293033a7c5ace5869cc91812fb509bfe08172ec Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 16:42:19 +0200 Subject: [PATCH 5/8] Update src/elementary-number-theory/ring-of-rational-numbers.lagda.md Co-authored-by: Fredrik Bakke --- .../ring-of-rational-numbers.lagda.md | 25 +++++++++++-------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md index d55eb180ed..b80164bffc 100644 --- a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md @@ -38,9 +38,9 @@ equipped with a [commutative](commutative-algebra.commutative-rings.md) [ring](ring-theory.rings.md). -## Lemmas +## Definitions -### The abelian group of rational numbers has a compatible multiplicative structure +### The compatible multiplicative structure on the abelian group of rational numbers ```agda has-associative-mul-ℚ : has-associative-mul ℚ @@ -52,21 +52,24 @@ pr1 is-unital-mul-ℚ = one-ℚ pr1 (pr2 is-unital-mul-ℚ) = left-unit-law-mul-ℚ pr2 (pr2 is-unital-mul-ℚ) = right-unit-law-mul-ℚ -has-mul-Ab-ℚ : has-mul-Ab ℚ-Ab -pr1 has-mul-Ab-ℚ = has-associative-mul-ℚ -pr1 (pr2 has-mul-Ab-ℚ) = is-unital-mul-ℚ -pr1 (pr2 (pr2 has-mul-Ab-ℚ)) = left-distributive-mul-add-ℚ -pr2 (pr2 (pr2 has-mul-Ab-ℚ)) = right-distributive-mul-add-ℚ +has-mul-ℚ-Ab : has-mul-Ab ℚ-Ab +pr1 has-mul-ℚ-Ab = has-associative-mul-ℚ +pr1 (pr2 has-mul-ℚ-Ab) = is-unital-mul-ℚ +pr1 (pr2 (pr2 has-mul-ℚ-Ab)) = left-distributive-mul-add-ℚ +pr2 (pr2 (pr2 has-mul-ℚ-Ab)) = right-distributive-mul-add-ℚ ``` -## Definitions - -### The commutative ring of rational numbers +### The ring of rational numbers ```agda ℚ-Ring : Ring lzero pr1 ℚ-Ring = ℚ-Ab -pr2 ℚ-Ring = has-mul-Ab-ℚ +pr2 ℚ-Ring = has-mul-ℚ-Ab +``` + +### The commutative ring of rational numbers + +```agda ℚ-Commutative-Ring : Commutative-Ring lzero pr1 ℚ-Commutative-Ring = ℚ-Ring From 037ab403fa8e1f06cd20bbdd45b90deb97356327 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 16:44:18 +0200 Subject: [PATCH 6/8] lint --- src/elementary-number-theory/ring-of-rational-numbers.lagda.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md index b80164bffc..acb9d10225 100644 --- a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md @@ -70,7 +70,6 @@ pr2 ℚ-Ring = has-mul-ℚ-Ab ### The commutative ring of rational numbers ```agda - ℚ-Commutative-Ring : Commutative-Ring lzero pr1 ℚ-Commutative-Ring = ℚ-Ring pr2 ℚ-Commutative-Ring = commutative-mul-ℚ From adee90202e4222a8c4ecfc43318231e154ba8e4a Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 17:17:25 +0200 Subject: [PATCH 7/8] abstract multiplication properties rational numbers --- .../multiplication-rational-numbers.lagda.md | 337 +++++++++--------- 1 file changed, 174 insertions(+), 163 deletions(-) diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md index 383d71a3d5..58d20f9e03 100644 --- a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md @@ -61,25 +61,26 @@ module _ (x : ℚ) where - left-zero-law-mul-ℚ : zero-ℚ *ℚ x ＝ zero-ℚ - left-zero-law-mul-ℚ = - ( eq-ℚ-sim-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ zero-ℚ) (fraction-ℚ x)) - ( fraction-ℚ zero-ℚ) - ( eq-is-zero-ℤ - ( ap (mul-ℤ' one-ℤ) (left-zero-law-mul-ℤ (numerator-ℚ x))) - ( left-zero-law-mul-ℤ _))) ∙ - ( is-retraction-rational-fraction-ℚ zero-ℚ) - - right-zero-law-mul-ℚ : x *ℚ zero-ℚ ＝ zero-ℚ - right-zero-law-mul-ℚ = - ( eq-ℚ-sim-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ zero-ℚ)) - ( fraction-ℚ zero-ℚ) - ( eq-is-zero-ℤ - ( ap (mul-ℤ' one-ℤ) (right-zero-law-mul-ℤ (numerator-ℚ x))) - ( left-zero-law-mul-ℤ _))) ∙ - ( is-retraction-rational-fraction-ℚ zero-ℚ) + abstract + left-zero-law-mul-ℚ : zero-ℚ *ℚ x ＝ zero-ℚ + left-zero-law-mul-ℚ = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ zero-ℚ) (fraction-ℚ x)) + ( fraction-ℚ zero-ℚ) + ( eq-is-zero-ℤ + ( ap (mul-ℤ' one-ℤ) (left-zero-law-mul-ℤ (numerator-ℚ x))) + ( left-zero-law-mul-ℤ _))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) + + right-zero-law-mul-ℚ : x *ℚ zero-ℚ ＝ zero-ℚ + right-zero-law-mul-ℚ = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ zero-ℚ)) + ( fraction-ℚ zero-ℚ) + ( eq-is-zero-ℤ + ( ap (mul-ℤ' one-ℤ) (right-zero-law-mul-ℤ (numerator-ℚ x))) + ( left-zero-law-mul-ℤ _))) ∙ + ( is-retraction-rational-fraction-ℚ zero-ℚ) ``` ### If the product of two rational numbers is zero, the left or right factor is zero @@ -112,106 +113,111 @@ decide-is-zero-factor-is-zero-mul-ℚ x y H = ### Unit laws for multiplication on rational numbers ```agda -left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x -left-unit-law-mul-ℚ x = - ( eq-ℚ-sim-fraction-ℤ - ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x)) - ( fraction-ℚ x) - ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ - ( is-retraction-rational-fraction-ℚ x) - -right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x -right-unit-law-mul-ℚ x = - ( eq-ℚ-sim-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ) - ( fraction-ℚ x) - ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ - ( is-retraction-rational-fraction-ℚ x) +abstract + left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x + left-unit-law-mul-ℚ x = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x)) + ( fraction-ℚ x) + ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ + ( is-retraction-rational-fraction-ℚ x) + + right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x + right-unit-law-mul-ℚ x = + ( eq-ℚ-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ) + ( fraction-ℚ x) + ( right-unit-law-mul-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)) +abstract + 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-ℤ +abstract + 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-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ 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) - ( mul-fraction-ℤ (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-ℤ - ( 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)))) + ( 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)) +abstract + 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-ℚ +abstract + 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 @@ -221,95 +227,100 @@ 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)) - -swap-neg-mul-ℚ : (x y : ℚ) → x *ℚ (neg-ℚ y) ＝ (neg-ℚ x) *ℚ y -swap-neg-mul-ℚ x y = - ( right-negative-law-mul-ℚ x y) ∙ - ( inv (left-negative-law-mul-ℚ x y)) + abstract + 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)) + +abstract + 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)) + + swap-neg-mul-ℚ : (x y : ℚ) → x *ℚ (neg-ℚ y) ＝ (neg-ℚ x) *ℚ y + swap-neg-mul-ℚ x y = + ( right-negative-law-mul-ℚ x y) ∙ + ( inv (left-negative-law-mul-ℚ x y)) ``` ### Multiplication on rational numbers distributes over addition ```agda -left-distributive-mul-add-ℚ : - (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ (x *ℚ y) +ℚ (x *ℚ z) -left-distributive-mul-add-ℚ x y z = - eq-ℚ-sim-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) - ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) - ( transitive-sim-fraction-ℤ +abstract + left-distributive-mul-add-ℚ : + (x y z : ℚ) → x *ℚ (y +ℚ z) ＝ (x *ℚ y) +ℚ (x *ℚ z) + left-distributive-mul-add-ℚ x y z = + eq-ℚ-sim-fraction-ℤ ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) - ( mul-fraction-ℤ - ( fraction-ℚ x) - ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) ( transitive-sim-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ (y +ℚ z))) ( mul-fraction-ℤ ( fraction-ℚ x) ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) - ( add-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z))) ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) - ( sim-fraction-add-fraction-ℤ - ( sim-reduced-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))) - ( sim-reduced-fraction-ℤ - ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z)))) - ( left-distributive-mul-add-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z))) - ( sim-fraction-mul-fraction-ℤ - ( refl-sim-fraction-ℤ (fraction-ℚ x)) ( transitive-sim-fraction-ℤ - ( fraction-ℚ (y +ℚ z)) - ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) - ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) - ( symmetric-sim-fraction-ℤ - ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) - ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( mul-fraction-ℤ + ( fraction-ℚ x) + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( add-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z))) + ( add-fraction-ℤ (fraction-ℚ (x *ℚ y)) (fraction-ℚ (x *ℚ z))) + ( sim-fraction-add-fraction-ℤ ( sim-reduced-fraction-ℤ - (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))) - ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z)))))) - -right-distributive-mul-add-ℚ : - (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ (x *ℚ z) +ℚ (y *ℚ z) -right-distributive-mul-add-ℚ x y z = - ( commutative-mul-ℚ (x +ℚ y) z) ∙ - ( left-distributive-mul-add-ℚ z x y) ∙ - ( ap-add-ℚ (commutative-mul-ℚ z x) (commutative-mul-ℚ z y)) + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))) + ( sim-reduced-fraction-ℤ + ( mul-fraction-ℤ (fraction-ℚ x) (fraction-ℚ z)))) + ( left-distributive-mul-add-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z))) + ( sim-fraction-mul-fraction-ℤ + ( refl-sim-fraction-ℤ (fraction-ℚ x)) + ( transitive-sim-fraction-ℤ + ( fraction-ℚ (y +ℚ z)) + ( reduce-fraction-ℤ (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) + ( symmetric-sim-fraction-ℤ + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)) + ( reduce-fraction-ℤ + ( add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z))) + ( sim-reduced-fraction-ℤ + (add-fraction-ℤ (fraction-ℚ y) (fraction-ℚ z)))) + ( refl-sim-fraction-ℤ (fraction-ℚ (y +ℚ z)))))) + + right-distributive-mul-add-ℚ : + (x y z : ℚ) → (x +ℚ y) *ℚ z ＝ (x *ℚ z) +ℚ (y *ℚ z) + right-distributive-mul-add-ℚ x y z = + ( commutative-mul-ℚ (x +ℚ y) z) ∙ + ( left-distributive-mul-add-ℚ z x y) ∙ + ( ap-add-ℚ (commutative-mul-ℚ z x) (commutative-mul-ℚ z y)) ``` ### Multiplication on rational numbers distributes over the difference ```agda -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)) +abstract + 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)) ``` From 751e4b8198c8aa3974d6dc22fc46989abef417c4 Mon Sep 17 00:00:00 2001 From: malarbol Date: Thu, 11 Apr 2024 17:22:13 +0200 Subject: [PATCH 8/8] fix header `ring-of-rational-numbers` --- src/elementary-number-theory/ring-of-rational-numbers.lagda.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md index acb9d10225..38ab1be037 100644 --- a/src/elementary-number-theory/ring-of-rational-numbers.lagda.md +++ b/src/elementary-number-theory/ring-of-rational-numbers.lagda.md @@ -35,8 +35,7 @@ The [commutative group of rational numbers](elementary-number-theory.group-of-rational-numbers.md) equipped with [multiplication](elementary-number-theory.multiplication-rational-numbers.md) is -a [commutative](commutative-algebra.commutative-rings.md) -[ring](ring-theory.rings.md). +a [commutative ring](commutative-algebra.commutative-rings.md). ## Definitions