123456789101112131415161718192021222324252627282930313233343536373839404142-------------------------------------------------------------------------- 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 Gopen 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 ⁻¹ ≈ yxyx⁻¹≈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) ⁻¹ ∎