diff options
| -rw-r--r-- | src/Helium/Algebra/Field.agda | 22 |
1 files changed, 22 insertions, 0 deletions
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 |