------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (AbelianGroup)
module Algebra.Properties.AbelianGroup
{a ℓ} (G : AbelianGroup a ℓ) where
open import Function.Base using (_$_)
open AbelianGroup G
open import Relation.Binary.Reasoning.Setoid setoid
------------------------------------------------------------------------
-- Publicly re-export group properties
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 _ _ ⟩
y ∙ x ∙ x ⁻¹ ≈⟨ assoc _ _ _ ⟩
y ∙ (x ∙ x ⁻¹) ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
y ∙ ε ≈⟨ identityʳ _ ⟩
y ∎
⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
x ⁻¹ ∙ y ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ y x ⟨
(y ∙ x) ⁻¹ ≈⟨ ⁻¹-cong $ comm y x ⟩
(x ∙ y) ⁻¹ ∎
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4