diff options
| author | Kazuhiko Sakaguchi | 2019-10-16 10:26:35 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | e7df10a74264f52a17f54f87b8a89c9360a46926 (patch) | |
| tree | 13e0a16336d9411d9de7a17110ed39467d7c95f5 /mathcomp/algebra/ssrint.v | |
| parent | f8d7a9f1090785a61dd81d745a0f46a24515f3d8 (diff) | |
Redefine `normedDomainType` (now `normedZmodType`) (#392)
* Redefine `normedDomainType` (now `normedZmodType`)
- Redefine `normedDomainType` to drop ring and integral domain axioms.
- Add canonical instance of `normedZmodType` for `prod`.
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index b408f9d..b85f0bc 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -434,7 +434,7 @@ Canonical int_porderType := POrderType ring_display int intOrdered.Mixin. Canonical int_latticeType := LatticeType int intOrdered.Mixin. Canonical int_orderType := OrderType int intOrdered.lez_total. Canonical int_numDomainType := NumDomainType int intOrdered.Mixin. -Canonical int_normedDomainType := NormedDomainType int int intOrdered.Mixin. +Canonical int_normedZmodType := NormedZmoduleType int int intOrdered.Mixin. Canonical int_realDomainType := [realDomainType of int]. Section intOrderedTheory. |