We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 7e2ec42 commit 6f03a34Copy full SHA for 6f03a34
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_compat ssralg ssrnum.
+From mathcomp Require Import all_ssreflect_compat 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