From 5f369e81edb641fc44efea990e451139eb70ced2 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 5 Jan 2026 13:10:16 -0500 Subject: [PATCH 1/9] adds additional properties to LeftModule --- CHANGELOG.md | 7 +++++ src/Algebra/Module/Properties/LeftModule.agda | 27 +++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e159cc52df..10ff8e2e70 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -155,6 +155,13 @@ Additions to existing modules ⊕-∧-booleanRing : BooleanRing _ _ ``` +* In `Algebra.Module.Properties.LeftModule`: + ```agda + -1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m + -‿distribˡ-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) + -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) + ``` + * In `Algebra.Properties.RingWithoutOne`: ```agda [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index ad6d33cc67..794dc946bb 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -23,3 +23,30 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public renaming (inverseˡ-unique to inverseˡ-uniqueᴹ ; inverseʳ-unique to inverseʳ-uniqueᴹ ; ⁻¹-involutive to -ᴹ-involutive) + +open import Algebra.Properties.Ring ring + +open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid + +-1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m +-1#*m≈-ᴹm m = uniqueʳ‿-ᴹ m (- 1# *ₗ m) (begin + m +ᴹ (- 1# *ₗ m) ≈⟨ +ᴹ-congʳ (*ₗ-identityˡ m) ⟨ + 1# *ₗ m +ᴹ (- 1# *ₗ m) ≈⟨ *ₗ-distribʳ m 1# (- 1#) ⟨ + (1# - 1#) *ₗ m ≈⟨ *ₗ-congʳ (-‿inverseʳ 1#) ⟩ + 0# *ₗ m ≈⟨ *ₗ-zeroˡ _ ⟩ + 0ᴹ ∎) + +-‿distribˡ-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) +-‿distribˡ-*ₗ r m = begin + - r *ₗ m ≈⟨ *ₗ-congʳ (-1*x≈-x _) ⟨ + (- 1# * r) *ₗ m ≈⟨ *ₗ-assoc _ _ _ ⟩ + (- 1#) *ₗ (r *ₗ m) ≈⟨ -1#*m≈-ᴹm _ ⟩ + -ᴹ (r *ₗ m ) ∎ + +-ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) +-ᴹ‿distrib-*ₗ r m = uniqueʳ‿-ᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) + (begin + r *ₗ m +ᴹ r *ₗ (-ᴹ m) ≈⟨ *ₗ-distribˡ r m (-ᴹ m) ⟨ + r *ₗ (m +ᴹ (-ᴹ m)) ≈⟨ *ₗ-congˡ (-ᴹ‿inverseʳ m) ⟩ + r *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ r ⟩ + 0ᴹ ∎) From c3b8f63ddda231b4c93728eef1d5d04c694f5757 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Thu, 8 Jan 2026 14:45:27 -0500 Subject: [PATCH 2/9] Update src/Algebra/Module/Properties/LeftModule.agda using suggestion Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Algebra/Module/Properties/LeftModule.agda | 26 +++++++++---------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index 794dc946bb..f690f5fe79 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -28,20 +28,12 @@ open import Algebra.Properties.Ring ring open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid --1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m --1#*m≈-ᴹm m = uniqueʳ‿-ᴹ m (- 1# *ₗ m) (begin - m +ᴹ (- 1# *ₗ m) ≈⟨ +ᴹ-congʳ (*ₗ-identityˡ m) ⟨ - 1# *ₗ m +ᴹ (- 1# *ₗ m) ≈⟨ *ₗ-distribʳ m 1# (- 1#) ⟨ - (1# - 1#) *ₗ m ≈⟨ *ₗ-congʳ (-‿inverseʳ 1#) ⟩ - 0# *ₗ m ≈⟨ *ₗ-zeroˡ _ ⟩ - 0ᴹ ∎) - --‿distribˡ-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) --‿distribˡ-*ₗ r m = begin - - r *ₗ m ≈⟨ *ₗ-congʳ (-1*x≈-x _) ⟨ - (- 1# * r) *ₗ m ≈⟨ *ₗ-assoc _ _ _ ⟩ - (- 1#) *ₗ (r *ₗ m) ≈⟨ -1#*m≈-ᴹm _ ⟩ - -ᴹ (r *ₗ m ) ∎ +-‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) +-‿distrib-*ₗ r m = uniqueʳ‿-ᴹ (r *ₗ m) (- r *ₗ m) (begin + r *ₗ m +ᴹ - r *ₗ m ≈⟨ *ₗ-distribʳ m r (- r) ⟨ + (r - r) *ₗ m ≈⟨ *ₗ-congʳ (-‿inverseʳ r) ⟩ + 0# *ₗ m ≈⟨ *ₗ-zeroˡ m ⟩ + 0ᴹ ∎) -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) -ᴹ‿distrib-*ₗ r m = uniqueʳ‿-ᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) @@ -50,3 +42,9 @@ open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid r *ₗ (m +ᴹ (-ᴹ m)) ≈⟨ *ₗ-congˡ (-ᴹ‿inverseʳ m) ⟩ r *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ r ⟩ 0ᴹ ∎) + +-1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m +-1#*m≈-ᴹm m = begin + - 1# *ₗ m ≈⟨ -‿distrib-*ₗ 1# m ⟩ + -ᴹ (1# *ₗ m) ≈⟨ -ᴹ‿cong (*ₗ-identityˡ m) ⟩ + -ᴹ m ∎ From 1bbc20509ceb9d1dc768d5d2f0be17b7470206bf Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 11:42:20 -0500 Subject: [PATCH 3/9] add subscript to name of lemma --- src/Algebra/Module/Properties/LeftModule.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index f690f5fe79..d36ccf5ee9 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -43,8 +43,8 @@ open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid r *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ r ⟩ 0ᴹ ∎) --1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m --1#*m≈-ᴹm m = begin +-1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m +-1#*ₗm≈-ᴹm m = begin - 1# *ₗ m ≈⟨ -‿distrib-*ₗ 1# m ⟩ -ᴹ (1# *ₗ m) ≈⟨ -ᴹ‿cong (*ₗ-identityˡ m) ⟩ -ᴹ m ∎ From 766ef7417a21ac2a61966fe79c31a8858422cce1 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 11:42:33 -0500 Subject: [PATCH 4/9] add RightModule properties --- CHANGELOG.md | 9 ++++++- .../Module/Properties/RightModule.agda | 26 +++++++++++++++++++ 2 files changed, 34 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 10ff8e2e70..357d96b021 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -157,11 +157,18 @@ Additions to existing modules * In `Algebra.Module.Properties.LeftModule`: ```agda - -1#*m≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m + -1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m -‿distribˡ-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) ``` +* In `Algebra.Module.Properties.RightModule`: + ```agda + -1#*ₗm≈-ᴹm : m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m + -‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r) + -ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r) + ``` + * In `Algebra.Properties.RingWithoutOne`: ```agda [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda index ef6b7c9f90..5ca725c632 100644 --- a/src/Algebra/Module/Properties/RightModule.agda +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -23,3 +23,29 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public renaming (inverseˡ-unique to inverseˡ-uniqueᴹ ; inverseʳ-unique to inverseʳ-uniqueᴹ ; ⁻¹-involutive to -ᴹ-involutive) + +open import Algebra.Properties.Ring ring + +open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid + +-‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r) +-‿distrib-*ᵣ m r = uniqueʳ‿-ᴹ (m *ᵣ r) (m *ᵣ - r) (begin + m *ᵣ r +ᴹ m *ᵣ - r ≈⟨ *ᵣ-distribˡ m r (- r) ⟨ + m *ᵣ (r - r) ≈⟨ *ᵣ-congˡ (-‿inverseʳ r) ⟩ + m *ᵣ 0# ≈⟨ *ᵣ-zeroʳ m ⟩ + 0ᴹ ∎) + +-ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r) +-ᴹ‿distrib-*ᵣ m r = uniqueʳ‿-ᴹ (m *ᵣ r) ((-ᴹ m) *ᵣ r) + (begin + m *ᵣ r +ᴹ (-ᴹ m) *ᵣ r ≈⟨ *ᵣ-distribʳ r m (-ᴹ m) ⟨ + (m +ᴹ -ᴹ m) *ᵣ r ≈⟨ *ᵣ-congʳ (-ᴹ‿inverseʳ m) ⟩ + 0ᴹ *ᵣ r ≈⟨ *ᵣ-zeroˡ r ⟩ + 0ᴹ ∎) + +m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m +m*ᵣ-1#≈-ᴹm m = begin + m *ᵣ (- 1#) ≈⟨ -‿distrib-*ᵣ m 1# ⟩ + -ᴹ (m *ᵣ 1#) ≈⟨ -ᴹ‿cong (*ᵣ-identityʳ m) ⟩ + -ᴹ m ∎ + From 7fb7db80b8055acd4c0b1ce96122cd64278ff429 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 17:52:43 -0500 Subject: [PATCH 5/9] Update src/Algebra/Module/Properties/RightModule.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Algebra/Module/Properties/RightModule.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda index 5ca725c632..742c8153ce 100644 --- a/src/Algebra/Module/Properties/RightModule.agda +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -29,7 +29,7 @@ open import Algebra.Properties.Ring ring open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r) --‿distrib-*ᵣ m r = uniqueʳ‿-ᴹ (m *ᵣ r) (m *ᵣ - r) (begin +-‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) (m *ᵣ - r) (begin m *ᵣ r +ᴹ m *ᵣ - r ≈⟨ *ᵣ-distribˡ m r (- r) ⟨ m *ᵣ (r - r) ≈⟨ *ᵣ-congˡ (-‿inverseʳ r) ⟩ m *ᵣ 0# ≈⟨ *ᵣ-zeroʳ m ⟩ From 7e9f6010fa803aa5bb8499a143306a14c487d3a5 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 17:53:05 -0500 Subject: [PATCH 6/9] Update CHANGELOG.md Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 357d96b021..f3b5c45659 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -158,7 +158,7 @@ Additions to existing modules * In `Algebra.Module.Properties.LeftModule`: ```agda -1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m - -‿distribˡ-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) + -‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) ``` From b3040749930dc76dbb9e0a7e8c26fa7e9bf8e689 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 17:53:30 -0500 Subject: [PATCH 7/9] Update src/Algebra/Module/Properties/LeftModule.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Algebra/Module/Properties/LeftModule.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index d36ccf5ee9..462e139510 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -29,7 +29,7 @@ open import Algebra.Properties.Ring ring open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m) --‿distrib-*ₗ r m = uniqueʳ‿-ᴹ (r *ₗ m) (- r *ₗ m) (begin +-‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (- r *ₗ m) (begin r *ₗ m +ᴹ - r *ₗ m ≈⟨ *ₗ-distribʳ m r (- r) ⟨ (r - r) *ₗ m ≈⟨ *ₗ-congʳ (-‿inverseʳ r) ⟩ 0# *ₗ m ≈⟨ *ₗ-zeroˡ m ⟩ From 9c86568a9fa6b253b4d02708efd9f16cf068ca6d Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 17:53:45 -0500 Subject: [PATCH 8/9] Update src/Algebra/Module/Properties/LeftModule.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Algebra/Module/Properties/LeftModule.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index 462e139510..74cc1d8148 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -36,8 +36,7 @@ open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid 0ᴹ ∎) -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m) --ᴹ‿distrib-*ₗ r m = uniqueʳ‿-ᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) - (begin +-ᴹ‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) (begin r *ₗ m +ᴹ r *ₗ (-ᴹ m) ≈⟨ *ₗ-distribˡ r m (-ᴹ m) ⟨ r *ₗ (m +ᴹ (-ᴹ m)) ≈⟨ *ₗ-congˡ (-ᴹ‿inverseʳ m) ⟩ r *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ r ⟩ From 5015eadc2838ad332483f715894237ee75f957b8 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Mon, 12 Jan 2026 17:53:57 -0500 Subject: [PATCH 9/9] Update src/Algebra/Module/Properties/RightModule.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Algebra/Module/Properties/RightModule.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda index 742c8153ce..2f6deb7c74 100644 --- a/src/Algebra/Module/Properties/RightModule.agda +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -36,8 +36,7 @@ open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid 0ᴹ ∎) -ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r) --ᴹ‿distrib-*ᵣ m r = uniqueʳ‿-ᴹ (m *ᵣ r) ((-ᴹ m) *ᵣ r) - (begin +-ᴹ‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) ((-ᴹ m) *ᵣ r) (begin m *ᵣ r +ᴹ (-ᴹ m) *ᵣ r ≈⟨ *ᵣ-distribʳ r m (-ᴹ m) ⟨ (m +ᴹ -ᴹ m) *ᵣ r ≈⟨ *ᵣ-congʳ (-ᴹ‿inverseʳ m) ⟩ 0ᴹ *ᵣ r ≈⟨ *ᵣ-zeroˡ r ⟩