------------------------------------------------------------------------
-- 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 ∎
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