diff options
| -rw-r--r-- | src/Helium/Algebra/Field.agda | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Helium/Algebra/Field.agda b/src/Helium/Algebra/Field.agda index 3cc2fae..20f13f6 100644 --- a/src/Helium/Algebra/Field.agda +++ b/src/Helium/Algebra/Field.agda @@ -12,11 +12,11 @@ module _ (_≈_ : Rel A ℓ) where - record IsField (+ _*_ : Op₂ A) (- _⁻¹ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where + record IsField (+ _*_ : Op₂ A) (- : Op₁ A) (0# 1# : A) (_⁻¹ : ∀ x {≢0 : ¬ x ≈ 0#} → 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# + ⁻¹-cong : ∀ x y {x≢0 y≢0}→ x ≈ y → (x ⁻¹) {x≢0} ≈ (y ⁻¹) {y≢0} + ⁻¹-inverseˡ : ∀ x {x≢0#} → ((x ⁻¹) {x≢0#} * x) ≈ 1# + ⁻¹-inverseʳ : ∀ x {x≢0#} → (x * (x ⁻¹) {x≢0#}) ≈ 1# open IsCommutativeRing isCommutativeRing public |