blob: 20f13f62b32a0ef81bc3ff15a7b8c4c5be41763d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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) (_⁻¹ : ∀ x {≢0 : ¬ x ≈ 0#} → A) : Set (a ⊔ ℓ) where
field
isCommutativeRing : IsCommutativeRing _≈_ + _*_ - 0# 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
|
