aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/algebra/rat.v4
-rw-r--r--mathcomp/algebra/ssrint.v2
-rw-r--r--mathcomp/algebra/ssrnum.v22
-rw-r--r--mathcomp/field/algC.v4
4 files changed, 16 insertions, 16 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 15cc4fc..14b5035 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -576,7 +576,7 @@ Canonical rat_porderType := POrderType ring_display rat ratLeMixin.
Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin.
Canonical rat_orderType := OrderType rat le_rat_total.
Canonical rat_numDomainType := NumDomainType rat ratLeMixin.
-Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin.
+Canonical rat_normedZmodType := NormedZmodType rat rat ratLeMixin.
Canonical rat_numFieldType := [numFieldType of rat].
Canonical rat_realDomainType := [realDomainType of rat].
Canonical rat_realFieldType := [realFieldType of rat].
@@ -811,7 +811,7 @@ Qed.
Require setoid_ring.Field_theory setoid_ring.Field_tac.
-Lemma rat_field_theory :
+Lemma rat_field_theory :
Field_theory.field_theory 0%Q 1%Q addq mulq subq oppq divq invq eq.
Proof.
split => //; first exact rat_ring_theory.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index fabe541..feaa884 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_distrLatticeType := DistrLatticeType int intOrdered.Mixin.
Canonical int_orderType := OrderType int intOrdered.lez_total.
Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
-Canonical int_normedZmodType := NormedZmoduleType int int intOrdered.Mixin.
+Canonical int_normedZmodType := NormedZmodType int int intOrdered.Mixin.
Canonical int_realDomainType := [realDomainType of int].
Section intOrderedTheory.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 36adce0..d607291 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -26,7 +26,7 @@ From mathcomp Require Import ssralg poly.
(* normedZmodType R *)
(* == interface for a normed Zmodule structure indexed by *)
(* numDomainType R. *)
-(* NormedZmoduleType R T m *)
+(* NormedZmodType R T m *)
(* == pack the normed Zmodule mixin into a normedZmodType. *)
(* The carrier T must have an integral domain structure. *)
(* [normedZmodType R of T for S] *)
@@ -64,7 +64,7 @@ From mathcomp Require Import ssralg poly.
(* * ArchiField (A Real Field with the archimedean axiom) *)
(* archiFieldType == interface for an archimedean field. *)
(* ArchiFieldType T r *)
-(* == packs the archimeadean axiom r into an archiFieldType. *)
+(* == packs the archimedean axiom r into an archiFieldType. *)
(* The carrier T must have a real field type structure. *)
(* [archiFieldType of T for S] *)
(* == T-clone of the archiFieldType structure S. *)
@@ -310,8 +310,8 @@ Canonical zmodType.
Coercion numDomain_normedZmodType : NumDomain.type >-> type.
Canonical numDomain_normedZmodType.
Notation normedZmodType R := (type (Phant R)).
-Notation NormedZmoduleType R T m := (@pack _ (Phant R) T _ m).
-Notation NormedZmoduleMixin := Mixin.
+Notation NormedZmodType R T m := (@pack _ (Phant R) T _ m).
+Notation NormedZmodMixin := Mixin.
Notation "[ 'normedZmodType' R 'of' T 'for' cT ]" :=
(@clone _ (Phant R) T cT _ idfun)
(at level 0, format "[ 'normedZmodType' R 'of' T 'for' cT ]") :
@@ -548,7 +548,7 @@ Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
Definition porderType := @Order.POrder.Pack ring_display cT xclass.
Definition numDomainType := @NumDomain.Pack cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition porder_fieldType := @GRing.Field.Pack porderType xclass.
Definition normedZmod_fieldType :=
@GRing.Field.Pack normedZmodType xclass.
@@ -648,7 +648,7 @@ Definition fieldType := @GRing.Field.Pack cT xclass.
Definition numFieldType := @NumField.Pack cT xclass.
Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
Definition closedFieldType := @GRing.ClosedField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition porder_decFieldType := @GRing.DecidableField.Pack porderType xclass.
Definition normedZmod_decFieldType :=
@GRing.DecidableField.Pack normedZmodType xclass.
@@ -764,7 +764,7 @@ Definition porderType := @Order.POrder.Pack ring_display cT xclass.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass.
Definition orderType := @Order.Total.Pack ring_display cT xclass.
Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition zmod_distrLatticeType :=
@Order.DistrLattice.Pack ring_display zmodType xclass.
Definition ring_distrLatticeType :=
@@ -897,7 +897,7 @@ Definition orderType := @Order.Total.Pack ring_display cT xclass.
Definition realDomainType := @RealDomain.Pack cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
Definition numFieldType := @NumField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition field_distrLatticeType :=
@Order.DistrLattice.Pack ring_display fieldType xclass.
Definition field_orderType := @Order.Total.Pack ring_display fieldType xclass.
@@ -996,7 +996,7 @@ Definition realDomainType := @RealDomain.Pack cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
Definition numFieldType := @NumField.Pack cT xclass.
Definition realFieldType := @RealField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
End ClassDef.
@@ -1084,7 +1084,7 @@ Definition realDomainType := @RealDomain.Pack cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
Definition numFieldType := @NumField.Pack cT xclass.
Definition realFieldType := @RealField.Pack cT xclass.
-Definition normedZmodType := NormedZmoduleType numDomainType cT xclass.
+Definition normedZmodType := NormedZmodType numDomainType cT xclass.
End ClassDef.
@@ -5064,7 +5064,7 @@ Definition normedZmodMixin :
@normed_mixin_of R [zmodType of U * V] (Num.RealDomain.class R) :=
@Num.NormedMixin _ _ _ norm normD norm_eq0 normrMn normrN.
-Canonical normedZmodType := NormedZmoduleType R (U * V) normedZmodMixin.
+Canonical normedZmodType := NormedZmodType R (U * V) normedZmodMixin.
Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|. Proof. by []. Qed.
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index aee2b85..0e3005d 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -232,7 +232,7 @@ Canonical closedFieldType := ClosedFieldType type closedFieldAxiom.
Parameter numMixin : numMixin idomainType.
Canonical porderType := POrderType ring_display type numMixin.
Canonical numDomainType := NumDomainType type numMixin.
-Canonical normedZmodType := NormedZmoduleType type type numMixin.
+Canonical normedZmodType := NormedZmodType type type numMixin.
Canonical numFieldType := [numFieldType of type].
Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType.
@@ -432,7 +432,7 @@ Definition numMixin : numMixin closedFieldType :=
sval (ComplexNumMixin conjK conj_nt).
Canonical porderType := POrderType ring_display type numMixin.
Canonical numDomainType := NumDomainType type numMixin.
-Canonical normedZmodType := NormedZmoduleType type type numMixin.
+Canonical normedZmodType := NormedZmodType type type numMixin.
Canonical numFieldType := [numFieldType of type].
Lemma normK u : `|u| ^+ 2 = u * conj u.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:18:10 +0000