diff options
Diffstat (limited to 'mathcomp/field/falgebra.v')
| -rw-r--r-- | mathcomp/field/falgebra.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 995dbee..e0ae1b1 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -641,12 +641,12 @@ Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id) Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun) (at level 0, format "[ 'aspace' 'of' U 'for' A ]") : form_scope. -Implicit Arguments prodvP [K aT U V W]. -Implicit Arguments cent1vP [K aT u v]. -Implicit Arguments centvP [K aT u V]. -Implicit Arguments centvsP [K aT U V]. -Implicit Arguments has_algidP [K aT U]. -Implicit Arguments polyOver1P [K aT p]. +Arguments prodvP [K aT U V W]. +Arguments cent1vP [K aT u v]. +Arguments centvP [K aT u V]. +Arguments centvsP [K aT U V]. +Arguments has_algidP [K aT U]. +Arguments polyOver1P [K aT p]. Section AspaceTheory. @@ -856,8 +856,8 @@ Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope. Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope. Notation "'Z ( A )" := (center_aspace A) : aspace_scope. -Implicit Arguments adim1P [K aT A]. -Implicit Arguments memv_cosetP [K aT U v w]. +Arguments adim1P [K aT A]. +Arguments memv_cosetP [K aT U v w]. Section Closure. @@ -1117,9 +1117,9 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f). End Class_Def. -Implicit Arguments ahom_in [aT rT]. -Implicit Arguments ahom_inP [aT rT f U]. -Implicit Arguments ahomP [aT rT f]. +Arguments ahom_in [aT rT]. +Arguments ahom_inP [aT rT f U]. +Arguments ahomP [aT rT f]. Section LRMorphism. @@ -1196,7 +1196,7 @@ Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f]. End AHom. -Implicit Arguments ahom_in [K aT rT]. +Arguments ahom_in [K aT rT]. Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope. Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope. |