chore(src/linear_algebra/free_module): rename file to free_module_pid (…

…#7805) In preparation for #7801
leanprover-community · Jun 3, 2021 · 2a93644 · 2a93644
1 parent fc6f967
commit 2a93644
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git 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 → src/linear_algebra/free_module_pid.lean b/src/linear_algebra/free_module.lean → 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;