diff options
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 486b12e..8e384a8 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1546,7 +1546,7 @@ End Exports. End Lmodule. Import Lmodule.Exports. -Definition scale (R : ringType) (V : lmodType R) := +Definition scale (R : ringType) (V : lmodType R) : R -> V -> V := Lmodule.scale (Lmodule.class V). Local Notation "*:%R" := (@scale _ _). |