← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Algebra/Properties/AbelianGroup.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Properties/AbelianGroup.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Some derivable properties
 
5
------------------------------------------------------------------------
 
6
 
 
7
open import Algebra
 
8
 
 
9
module Algebra.Properties.AbelianGroup
 
10
         {g₁ g₂} (G : AbelianGroup g₁ g₂) where
 
11
 
 
12
import Algebra.Properties.Group as GP
 
13
open import Data.Product
 
14
open import Function
 
15
import Relation.Binary.EqReasoning as EqR
 
16
 
 
17
open AbelianGroup G
 
18
open EqR setoid
 
19
 
 
20
open GP group public
 
21
 
 
22
private
 
23
  lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
 
24
  lemma x y = begin
 
25
    x ∙ y ∙ x ⁻¹    ≈⟨ comm _ _ ⟨ ∙-cong ⟩ refl ⟩
 
26
    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
 
27
    y ∙ (x ∙ x ⁻¹)  ≈⟨ refl ⟨ ∙-cong ⟩ proj₂ inverse _ ⟩
 
28
    y ∙ ε           ≈⟨ proj₂ identity _ ⟩
 
29
    y               ∎
 
30
 
 
31
⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
 
32
⁻¹-∙-comm x y = begin
 
33
  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
 
34
  y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-cong ⟩ refl ⟩
 
35
  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩
 
36
  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma _ _ ⟩
 
37
  (x ∙ y) ⁻¹                          ∎
 
38
  where
 
39
  lem = begin
 
40
    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈⟨ sym $ assoc _ _ _ ⟩
 
41
    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈⟨ sym $ assoc _ _ _ ⟨ ∙-cong ⟩ refl ⟩
 
42
    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ proj₂ inverse _ ⟨ ∙-cong ⟩ refl ⟩
 
43
    ε ∙ y ⁻¹                     ≈⟨ proj₁ identity _ ⟩
 
44
    y ⁻¹                         ∎