[ new ] ⁻¹-anti-homo-(// | \\) (#2349)

* [ new ] ¹-anti-homo‿-

* Update CHANGELOG.md

Co-authored-by: Nathan van Doorn <[email protected]>

* Update src/Algebra/Properties/Group.agda

Co-authored-by: jamesmckinna <[email protected]>

* Update CHANGELOG.md

Co-authored-by: jamesmckinna <[email protected]>

* [ more ] symmetric lemma

* [ new ] ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x

---------

Co-authored-by: MatthewDaggitt <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>

Author: 4 people

CHANGELOG.md

@@ -236,6 +236,11 @@ Additions to existing modules
     record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
     record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
 
+* In `Algebra.Properties.AbelianGroup`:
+  ```
+  ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
+  ```
+
 * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
@@ -253,6 +258,8 @@ Additions to existing modules
   ⁻¹-selfInverse  : SelfInverse _⁻¹
   \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
   comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
+  ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x
+  ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x
   ```
 
 * In `Algebra.Properties.Loop`:

src/Algebra/Properties/AbelianGroup.agda

@@ -23,6 +23,9 @@ open import Algebra.Properties.Group group public
 ------------------------------------------------------------------------
 -- Properties of abelian groups
 
+⁻¹-anti-homo‿- : ∀ x y → (x - y) ⁻¹ ≈ y - x
+⁻¹-anti-homo‿- = ⁻¹-anti-homo-//
+
 xyx⁻¹≈y : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
 xyx⁻¹≈y x y = begin
   x ∙ y ∙ x ⁻¹    ≈⟨ ∙-congʳ $ comm _ _ ⟩

src/Algebra/Properties/Group.agda

@@ -126,6 +126,22 @@ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
   (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
   x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎
 
+⁻¹-anti-homo-// : ∀ x y → (x // y) ⁻¹ ≈ y // x
+⁻¹-anti-homo-// x y = begin
+  (x // y) ⁻¹      ≡⟨⟩
+  (x ∙ y ⁻¹) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
+  (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
+  y ∙ x ⁻¹         ≡⟨⟩
+  y // x ∎
+
+⁻¹-anti-homo-\\ : ∀ x y → (x \\ y) ⁻¹ ≈ y \\ x
+⁻¹-anti-homo-\\ x y = begin
+  (x \\ y) ⁻¹      ≡⟨⟩
+  (x ⁻¹ ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
+  y ⁻¹ ∙ (x ⁻¹) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
+  y ⁻¹ ∙ x         ≡⟨⟩
+  y \\ x ∎
+
 \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
 \\≗flip-//⇒comm \\≗//ᵒ x y = begin
   x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨