diff options
Diffstat (limited to 'src/Helium/Algebra/Structures.agda')
| -rw-r--r-- | src/Helium/Algebra/Structures.agda | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Helium/Algebra/Structures.agda b/src/Helium/Algebra/Structures.agda index b64b4c7..f88ce59 100644 --- a/src/Helium/Algebra/Structures.agda +++ b/src/Helium/Algebra/Structures.agda @@ -72,6 +72,7 @@ record IsDivisionRing (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ) where field +-isAbelianGroup : IsAbelianGroup + 0# -_ + -- FIXME: unroll definition *-isAlmostGroup : IsAlmostGroup _*_ 0# 1# _⁻¹ distrib : _*_ DistributesOver + zero : Zero 0# _*_ @@ -126,7 +127,9 @@ record IsDivisionRing isRing : IsRing + _*_ -_ 0# 1# isRing = record { +-isAbelianGroup = +-isAbelianGroup - ; *-isMonoid = *-isMonoid + ; *-cong = *-cong + ; *-assoc = *-assoc + ; *-identity = *-identity ; distrib = distrib ; zero = zero } |