From 4643e5107299a8f55a4f130c1da84d6011f1e017 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Thu, 16 Dec 2021 12:40:35 +0000
Subject: Introduce definition of a field.

---
 src/Helium/Algebra/Field.agda | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 src/Helium/Algebra/Field.agda

diff --git a/src/Helium/Algebra/Field.agda b/src/Helium/Algebra/Field.agda
new file mode 100644
index 0000000..3cc2fae
--- /dev/null
+++ b/src/Helium/Algebra/Field.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Helium.Algebra.Field where
+
+open import Algebra
+open import Level
+open import Relation.Binary
+open import Relation.Nullary
+
+module _
+  {a ℓ} {A : Set a}
+  (_≈_ : Rel A ℓ)
+  where
+
+  record IsField (+ _*_ : Op₂ A) (- _⁻¹ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+    field
+      isCommutativeRing : IsCommutativeRing _≈_ + _*_ - 0# 1#
+      ⁻¹-cong           : Congruent₁ _≈_ _⁻¹
+      ⁻¹-inverseˡ       : ∀ x → ¬ x ≈ 0# → ((x ⁻¹) * x) ≈ 1#
+      ⁻¹-inverseʳ       : ∀ x → ¬ x ≈ 0# → (x * (x ⁻¹)) ≈ 1#
+
+    open IsCommutativeRing isCommutativeRing public
-- 
cgit v1.2.3