Skip to content

Commit 7bec9fe

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

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
@@ -40,7 +40,7 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
4040
(* K is a numDomainType. *)
4141
(* UniformLmodule K == HB class, join of UniformNmodule and Lmodule *)
4242
(* with a uniformly continuous scaling operation *)
43-
(* K is a numFieldType *)
43+
(* K is a numFieldType. *)
4444
(* convexTvsType R == interface type for a locally convex *)
4545
(* tvs on a numDomain R *)
4646
(* A convex tvs is constructed over a uniform *)

0 commit comments

Comments
 (0)