------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of Rings ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (Ring) module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where open Ring R import Algebra.Properties.RingWithoutOne as RingWithoutOneProperties open import Function.Base using (_$_) open import Relation.Binary.Reasoning.Setoid setoid open import Algebra.Definitions _≈_ ------------------------------------------------------------------------ -- Export properties of rings without a 1#. open RingWithoutOneProperties ringWithoutOne public ------------------------------------------------------------------------ -- Extra properties of 1# -1*x≈-x : ∀ x → - 1# * x ≈ - x -1*x≈-x x = begin - 1# * x ≈⟨ -‿distribˡ-* 1# x ⟨ - (1# * x) ≈⟨ -‿cong ( *-identityˡ x ) ⟩ - x ∎