Skip to content

Commit 62418bb

Browse files
affeldt-aistmkerjean
authored andcommitted
Apply suggestion from @affeldt-aist
1 parent fb543b2 commit 62418bb

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • theories/normedtype_theory

theories/normedtype_theory/tvs.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
3737
(* UniformZmodule == HB class, join of UniformNmodule and Zmodule *)
3838
(* with uniformly continuous opposite operator *)
3939
(* PreUniformLmodule K == HB class, join of Uniform and Lmodule over K *)
40-
(* K is a numDomainType *)
40+
(* K is a numDomainType. *)
4141
(* UniformLmodule K == HB class, join of UniformNmodule and Lmodule *)
4242
(* with a uniformly continuous scaling operation *)
4343
(* K is a numFieldType *)

0 commit comments

Comments
 (0)