We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 994f950 commit 1a0fa98Copy full SHA for 1a0fa98
1 file changed
theories/normedtype_theory/complete_normed_module.v
@@ -1,6 +1,6 @@
1
(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *)
2
From HB Require Import structures.
3
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import all_ssreflect ssralg ssrnum vector.
4
From mathcomp Require Import boolp classical_sets interval_inference reals.
5
From mathcomp Require Import topology tvs pseudometric_normed_Zmodule.
6
From mathcomp Require Import normed_module.
0 commit comments