diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-19 09:18:45 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-19 09:18:45 +0000 |
| commit | 4e617e45594c6a272678923878319fc7f1584452 (patch) | |
| tree | 377a5462f1479c292d85b9747707bdcc5e57388c | |
| parent | 4643e5107299a8f55a4f130c1da84d6011f1e017 (diff) | |
Modify multiplicative inverse to not require zero.
| -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 |