1234567891011121314151617181920212223242526272829303132333435363738394041-------------------------------------------------------------------------- The Agda standard library---- Some derivable properties------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra module Algebra.Properties.AbelianGroup {a ℓ} (G : AbelianGroup a ℓ) where open AbelianGroup Gopen import Function.Base using (_$_)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 ⁻¹ ≈ 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) ⁻¹ ∎