diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 14:18:28 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 14:18:28 +0100 |
| commit | ba95dc7d15cab1af40da896114b7dd9aad5afda0 (patch) | |
| tree | 86a18163a575083a976eda69ee2d79aecde9fe7c /src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda | |
| parent | efdd7c70a8605c51b7aaa1b0b33914ca741ffe39 (diff) | |
Add some properties of ordered fields.
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda')
| -rw-r--r-- | src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda index 0f8df22..648d164 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -567,7 +567,7 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ( +-rawMagma; +-rawMonoid ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup ; rawSemiring; rawRing - ; semiring; ring; divisionRing + ; semiring; commutativeSemiring; ring; commutativeRing; divisionRing ) open IsField.Unordered isField public |