blob: 3cc2faecdf3d9171c5123138ad92ef2d4aba1b82 (
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) : 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
|
