diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index ca77f0c90b4ac..4b4f72d49a09c 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
-import linear_algebra.free_module
+import linear_algebra.free_module_pid
 import linear_algebra.matrix.basis
 import linear_algebra.matrix.diagonal
 import linear_algebra.matrix.to_linear_equiv
diff --git a/src/linear_algebra/free_module.lean b/src/linear_algebra/free_module_pid.lean
similarity index 99%
rename from src/linear_algebra/free_module.lean
rename to src/linear_algebra/free_module_pid.lean
index 21c0e3e0861a6..a34a2a165d238 100644
--- a/src/linear_algebra/free_module.lean
+++ b/src/linear_algebra/free_module_pid.lean
@@ -8,13 +8,14 @@ import linear_algebra.finsupp_vector_space
 import ring_theory.principal_ideal_domain
 import ring_theory.finiteness
 
-/-! # Free modules
+/-! # Free modules over PID
 
 A free `R`-module `M` is a module with a basis over `R`,
 equivalently it is an `R`-module linearly equivalent to `ι →₀ R` for some `ι`.
 
 This file proves a submodule of a free `R`-module of finite rank is also
-a free `R`-module of finite rank, if `R` is a principal ideal domain.
+a free `R`-module of finite rank, if `R` is a principal ideal domain (PID),
+i.e. we have instances `[integral_domain R] [is_principal_ideal_ring R]`.
 We express "free `R`-module of finite rank" as a module `M` which has a basis
 `b : ι → R`, where `ι` is a `fintype`.
 We call the cardinality of `ι` the rank of `M` in this file;