chore: Rename FiniteDimensional.finrank to Module.finrank (#17192)

The namespacing in the linear algebra/affine spaces part of the library is a bit suboptimal. Here are a few arguments for why `FiniteDimensional.finrank` should be renamed to `Module.finrank`: 1. Other objects in maths can be finite-dimensional and have a rank. 2. `finrank` is directly analogous to `Module.rank`, they have lemmas in common (eg `finrank_eq_rank`, which is currently in neither of the declarations' namespaces) and have common series of lemmas that relate to other declarations in the `Module` namespace, eg `Module.Finite`. 3. We are in the process of replacing `FiniteDimensional` by `Module.Finite`, so the `FiniteDimensional` namespace will soon be obsolete. 4. It is a shorter and clearer name. Also make `Module.Finite` protected to avoid clashes with `Finite`
leanprover-community · Oct 3, 2024 · 0c13e18 · 0c13e18
1 parent 78d9855
commit 0c13e18
Show file tree

Hide file tree

Showing 168 changed files with 477 additions and 500 deletions.
diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -57,7 +57,7 @@ rather than more literally with `affineSegment`.
 -/
 
 
-open Affine Affine.Simplex EuclideanGeometry FiniteDimensional
+open Affine Affine.Simplex EuclideanGeometry Module
 
 open scoped Affine EuclideanGeometry Real
 

diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean
@@ -41,7 +41,7 @@ noncomputable section
 
 local notation "√" => Real.sqrt
 
-open Function Bool LinearMap Fintype FiniteDimensional Module.DualBases
+open Function Bool LinearMap Fintype Module Module.DualBases
 
 /-!
 ### The hypercube

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean b/Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean
@@ -12,7 +12,7 @@ If `A` is a domain, and a finite-dimensional algebra over a field `F`, with prim
 then there are no non-trivial `F`-subalgebras.
 -/
 
-open FiniteDimensional Submodule
+open Module Submodule
 
 theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A]
     [Algebra F A] (hp : (finrank F A).Prime) : IsSimpleOrder (Subalgebra F A) :=

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
@@ -18,7 +18,7 @@ satisfies strong rank condition, we put them into a separate file.
 
 -/
 
-open FiniteDimensional
+open Module
 
 namespace Subalgebra
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean
@@ -26,7 +26,7 @@ linear algebra, module, free
 
 -/
 
-open CategoryTheory
+open CategoryTheory Module
 
 namespace ModuleCat
 
@@ -177,11 +177,11 @@ theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃]
 
 theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃]
     [Module.Finite R S.X₁] [Module.Finite R S.X₃]
-    (hN : FiniteDimensional.finrank R S.X₁ = n)
-    (hP : FiniteDimensional.finrank R S.X₃ = p)
+    (hN : Module.finrank R S.X₁ = n)
+    (hP : Module.finrank R S.X₃ = p)
     [StrongRankCondition R] :
-    FiniteDimensional.finrank R S.X₂ = n + p := by
-  apply FiniteDimensional.finrank_eq_of_rank_eq
+    finrank R S.X₂ = n + p := by
+  apply finrank_eq_of_rank_eq
   rw [free_shortExact_rank_add hS', ← hN, ← hP]
   simp only [Nat.cast_add, finrank_eq_rank]
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Simple.lean b/Mathlib/Algebra/Category/ModuleCat/Simple.lean
@@ -34,7 +34,7 @@ instance simple_of_isSimpleModule [IsSimpleModule R M] : Simple (of R M) :=
 instance isSimpleModule_of_simple (M : ModuleCat R) [Simple M] : IsSimpleModule R M :=
   simple_iff_isSimpleModule.mp (Simple.of_iso (ofSelfIso M))
 
-open FiniteDimensional
+open Module
 
 attribute [local instance] moduleOfAlgebraModule isScalarTower_of_algebra_moduleCat
 

diff --git a/Mathlib/Algebra/Lie/CartanExists.lean b/Mathlib/Algebra/Lie/CartanExists.lean
@@ -39,7 +39,7 @@ variable [Module.Finite K L]
 variable [Module.Finite R L] [Module.Free R L]
 variable [Module.Finite R M] [Module.Free R M]
 
-open FiniteDimensional LieSubalgebra Module.Free Polynomial
+open Module LieSubalgebra Module.Free Polynomial
 
 variable (K)
 
@@ -117,7 +117,7 @@ section Field
 
 variable {K L : Type*} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L]
 
-open FiniteDimensional LieSubalgebra LieSubmodule Polynomial Cardinal LieModule engel_isBot_of_isMin
+open Module LieSubalgebra LieSubmodule Polynomial Cardinal LieModule engel_isBot_of_isMin
 
 #adaptation_note /-- otherwise there is a spurious warning on `contrapose!` below. -/
 set_option linter.unusedVariables false in
@@ -360,7 +360,7 @@ lemma exists_isCartanSubalgebra_engel_of_finrank_le_card (h : finrank K L ≤ #K
   suffices finrank K (engel K x) ≤ finrank K (engel K y) by
     suffices engel K y = engel K x from this.ge
     apply LieSubalgebra.to_submodule_injective
-    exact eq_of_le_of_finrank_le hyx this
+    exact Submodule.eq_of_le_of_finrank_le hyx this
   rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]
   apply rank_le_finrank_engel
 

diff --git a/Mathlib/Algebra/Lie/InvariantForm.lean b/Mathlib/Algebra/Lie/InvariantForm.lean
@@ -124,14 +124,14 @@ variable (hΦ_inv : Φ.lieInvariant L) (hΦ_refl : Φ.IsRefl)
 variable (hL : ∀ I : LieIdeal K L, IsAtom I → ¬IsLieAbelian I)
 include hΦ_nondeg hΦ_refl hL
 
-open FiniteDimensional Submodule in
+open Module Submodule in
 lemma orthogonal_isCompl_coe_submodule (I : LieIdeal K L) (hI : IsAtom I) :
     IsCompl I.toSubmodule (orthogonal Φ hΦ_inv I).toSubmodule := by
   rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl,
       ← orthogonal_toSubmodule _ hΦ_inv, ← LieSubmodule.disjoint_iff_coe_toSubmodule]
   exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI
 
-open FiniteDimensional Submodule in
+open Module Submodule in
 lemma orthogonal_isCompl (I : LieIdeal K L) (hI : IsAtom I) :
     IsCompl I (orthogonal Φ hΦ_inv I) := by
   rw [LieSubmodule.isCompl_iff_coe_toSubmodule]
@@ -151,7 +151,7 @@ lemma restrict_orthogonal_nondegenerate (I : LieIdeal K L) (hI : IsAtom I) :
     LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]
   exact (orthogonal_isCompl_coe_submodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm
 
-open FiniteDimensional Submodule in
+open Module Submodule in
 lemma atomistic : ∀ I : LieIdeal K L, sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I := by
   intro I
   apply le_antisymm

diff --git a/Mathlib/Algebra/Lie/Rank.lean b/Mathlib/Algebra/Lie/Rank.lean
@@ -65,13 +65,13 @@ lemma rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] :
     rank R L M = (polyCharpoly φ b).natTrailingDegree := by
   apply nilRank_eq_polyCharpoly_natTrailingDegree
 
-open FiniteDimensional
+open Module
 
 include bₘ in
 lemma rank_le_card [Nontrivial R] : rank R L M ≤ Fintype.card ιₘ :=
   nilRank_le_card _ bₘ
 
-open FiniteDimensional
+open Module
 lemma rank_le_finrank [Nontrivial R] : rank R L M ≤ finrank R M :=
   nilRank_le_finrank _
 
@@ -103,7 +103,7 @@ section IsDomain
 variable (L)
 variable [IsDomain R]
 
-open Cardinal FiniteDimensional MvPolynomial in
+open Cardinal Module MvPolynomial in
 lemma exists_isRegular_of_finrank_le_card (h : finrank R M ≤ #R) :
     ∃ x : L, IsRegular R M x :=
   LinearMap.exists_isNilRegular_of_finrank_le_card _ h
@@ -138,7 +138,7 @@ lemma rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] :
     rank R L = (polyCharpoly (ad R L).toLinearMap b).natTrailingDegree := by
   apply nilRank_eq_polyCharpoly_natTrailingDegree
 
-open FiniteDimensional
+open Module
 
 include b in
 lemma rank_le_card [Nontrivial R] : rank R L ≤ Fintype.card ι :=
@@ -175,7 +175,7 @@ section IsDomain
 variable (L)
 variable [IsDomain R]
 
-open Cardinal FiniteDimensional MvPolynomial in
+open Cardinal Module MvPolynomial in
 lemma exists_isRegular_of_finrank_le_card (h : finrank R L ≤ #R) :
     ∃ x : L, IsRegular R x :=
   LinearMap.exists_isNilRegular_of_finrank_le_card _ h
@@ -191,7 +191,7 @@ namespace LieAlgebra
 
 variable (K : Type*) {L : Type*} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L]
 
-open FiniteDimensional LieSubalgebra
+open Module LieSubalgebra
 
 lemma finrank_engel (x : L) :
     finrank K (engel K x) = (ad K L x).charpoly.natTrailingDegree :=

diff --git a/Mathlib/Algebra/Lie/TraceForm.lean b/Mathlib/Algebra/Lie/TraceForm.lean
@@ -38,7 +38,7 @@ variable (R K L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
 local notation "φ" => LieModule.toEnd R L M
 
 open LinearMap (trace)
-open Set FiniteDimensional
+open Set Module
 
 namespace LieModule
 
@@ -392,7 +392,7 @@ lemma killingForm_eq :
 
 end LieIdeal
 
-open LieModule FiniteDimensional
+open LieModule Module
 open Submodule (span subset_span)
 
 namespace LieModule

diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean
@@ -745,7 +745,7 @@ lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) :
   simp_rw [Module.End.maxGenEigenspace_def]
   exact IsTriangularizable.iSup_eq_top x
 
-open LinearMap FiniteDimensional in
+open LinearMap Module in
 @[simp]
 lemma trace_toEnd_genWeightSpace [IsDomain R] [IsPrincipalIdealRing R]
     [Module.Free R M] [Module.Finite R M] (χ : L → R) (x : L) :
@@ -759,7 +759,7 @@ lemma trace_toEnd_genWeightSpace [IsDomain R] [IsPrincipalIdealRing R]
 
 section field
 
-open FiniteDimensional
+open Module
 
 variable (K)
 variable [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.IsNilpotent K L]

diff --git a/Mathlib/Algebra/Lie/Weights/Chain.lean b/Mathlib/Algebra/Lie/Weights/Chain.lean
@@ -41,7 +41,7 @@ We provide basic definitions and results to support `α`-chain techniques in thi
 
 -/
 
-open FiniteDimensional Function Set
+open Module Function Set
 
 variable {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L]
   (M : Type*) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

diff --git a/Mathlib/Algebra/Lie/Weights/Killing.lean b/Mathlib/Algebra/Lie/Weights/Killing.lean
@@ -85,7 +85,7 @@ end IsKilling
 
 section Field
 
-open FiniteDimensional LieModule Set
+open Module LieModule Set
 open Submodule (span subset_span)
 
 variable [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra]

diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean
@@ -114,7 +114,7 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R
 
 section FiniteDimensional
 
-open FiniteDimensional
+open Module
 
 variable [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
   [LieAlgebra.IsNilpotent R L]

diff --git a/Mathlib/Algebra/Module/LinearMap/Polynomial.lean b/Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@@ -351,7 +351,7 @@ lemma polyCharpolyAux_basisIndep {ιM' : Type*} [Fintype ιM'] [DecidableEq ιM'
 
 end aux
 
-open FiniteDimensional Matrix
+open Module Matrix
 
 variable [Module.Free R M] [Module.Finite R M] (b : Basis ι R L)
 
@@ -479,11 +479,11 @@ lemma polyCharpoly_coeff_nilRank_ne_zero :
   rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b]
   apply polyCharpoly_coeff_nilRankAux_ne_zero
 
-open FiniteDimensional Module.Free
+open Module Module.Free
 
 lemma nilRank_le_card {ι : Type*} [Fintype ι] (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι := by
   apply Polynomial.natTrailingDegree_le_of_ne_zero
-  rw [← FiniteDimensional.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
+  rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
     Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]
   apply one_ne_zero
 
@@ -538,7 +538,7 @@ section IsDomain
 
 variable [IsDomain R]
 
-open Cardinal FiniteDimensional MvPolynomial Module.Free in
+open Cardinal Module MvPolynomial Module.Free in
 lemma exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) :
     ∃ x : L, IsNilRegular φ x := by
   let b := chooseBasis R L

diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -104,7 +104,7 @@ theorem map_mono {f : F} {p p' : Submodule R M} : p ≤ p' → map f p ≤ map f
   image_subset _
 
 @[simp]
-theorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥ :=
+protected theorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥ :=
   have : ∃ x : M, x ∈ p := ⟨0, p.zero_mem⟩
   ext <| by simp [this, eq_comm]
 

diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean
@@ -384,7 +384,7 @@ end ZSpan
 
 section ZLattice
 
-open Submodule FiniteDimensional ZSpan
+open Submodule Module ZSpan
 
 -- TODO: generalize this class to other rings than `ℤ`
 /-- `L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if
@@ -562,7 +562,7 @@ variable {ι : Type*} [hs : IsZLattice K L] (b : Basis ι ℤ L)
 /-- Any `ℤ`-basis of `L` is also a `K`-basis of `E`. -/
 def Basis.ofZLatticeBasis :
     Basis ι K E := by
-  have : Finite ℤ L := ZLattice.module_finite K L
+  have : Module.Finite ℤ L := ZLattice.module_finite K L
   have : Free ℤ L := ZLattice.module_free K L
   let e :=  Basis.indexEquiv (Free.chooseBasis ℤ L) b
   have : Fintype ι := Fintype.ofEquiv _ e

diff --git a/Mathlib/Algebra/Module/ZLattice/Covolume.lean b/Mathlib/Algebra/Module/ZLattice/Covolume.lean
@@ -29,7 +29,7 @@ noncomputable section
 
 namespace ZLattice
 
-open Submodule MeasureTheory FiniteDimensional MeasureTheory Module
+open Submodule MeasureTheory Module MeasureTheory Module
 
 section General
 

diff --git a/Mathlib/Algebra/Polynomial/Module/AEval.lean b/Mathlib/Algebra/Polynomial/Module/AEval.lean
@@ -46,7 +46,8 @@ instance instAddCommMonoid : AddCommMonoid <| AEval R M a := inferInstanceAs (Ad
 
 instance instModuleOrig : Module R <| AEval R M a := inferInstanceAs (Module R M)
 
-instance instFiniteOrig [Finite R M] : Finite R <| AEval R M a := inferInstanceAs (Finite R M)
+instance instFiniteOrig [Module.Finite R M] : Module.Finite R <| AEval R M a :=
+  ‹Module.Finite R M›
 
 instance instModulePolynomial : Module R[X] <| AEval R M a := compHom M (aeval a).toRingHom
 
@@ -79,7 +80,7 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w
     apply (of R M a).symm.injective
     rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
 
-instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
+instance instFinitePolynomial [Module.Finite R M] : Module.Finite R[X] <| AEval R M a :=
   Finite.of_restrictScalars_finite R _ _
 
 /-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
@@ -193,6 +194,6 @@ lemma AEval'.X_smul_of (m : M) : (X : R[X]) • AEval'.of φ m = AEval'.of φ (
 lemma AEval'.of_symm_X_smul (m : AEval' φ) :
     (AEval'.of φ).symm ((X : R[X]) • m) = φ ((AEval'.of φ).symm m) := AEval.of_symm_X_smul _ _
 
-instance [Finite R M] : Finite R[X] <| AEval' φ := inferInstance
+instance [Module.Finite R M] : Module.Finite R[X] <| AEval' φ := inferInstance
 
 end Module
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -569,8 +569,8 @@ theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R,c₁,c₂] =
   rw [rank_eq_card_basis (basisOneIJK c₁ c₂), Fintype.card_fin]
   norm_num
 
-theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4 := by
-  rw [FiniteDimensional.finrank, rank_eq_four, Cardinal.toNat_ofNat]
+theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R,c₁,c₂] = 4 := by
+  rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]
 
 /-- There is a natural equivalence when swapping the coefficients of a quaternion algebra. -/
 @[simps]
@@ -1024,7 +1024,7 @@ instance : Module.Free R ℍ[R] := inferInstanceAs <| Module.Free R ℍ[R,-1,-1]
 theorem rank_eq_four [StrongRankCondition R] : Module.rank R ℍ[R] = 4 :=
   QuaternionAlgebra.rank_eq_four _ _
 
-theorem finrank_eq_four [StrongRankCondition R] : FiniteDimensional.finrank R ℍ[R] = 4 :=
+theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R] = 4 :=
   QuaternionAlgebra.finrank_eq_four _ _
 
 @[simp] theorem star_re : (star a).re = a.re := rfl

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
@@ -545,7 +545,7 @@ lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 := by
       rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
         ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
         (CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq,
-        FiniteDimensional.finrank_self]
+        Module.finrank_self]
   · exact congr_arg toClass
 
 lemma toClass_injective : Function.Injective <| @toClass _ _ W := by

diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean b/Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean
@@ -115,7 +115,7 @@ theorem ae_convolution_tendsto_right_of_locallyIntegrable
     tendsto_nhdsWithin_iff.2 ⟨hφ, Eventually.of_forall (fun i ↦ (φ i).rOut_pos)⟩
   have := (h₀.comp (Besicovitch.tendsto_filterAt μ x₀)).comp hφ'
   simp only [Function.comp] at this
-  apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (FiniteDimensional.finrank ℝ G)) this
+  apply tendsto_integral_smul_of_tendsto_average_norm_sub (K ^ (Module.finrank ℝ G)) this
   · filter_upwards with i using
       hg.integrableOn_isCompact (isCompact_closedBall _ _)
   · apply tendsto_const_nhds.congr (fun i ↦ ?_)

diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
@@ -25,7 +25,7 @@ the indicator function of `closedBall 0 1` with a function as above with `s = ba
 
 noncomputable section
 
-open Set Metric TopologicalSpace Function Asymptotics MeasureTheory FiniteDimensional
+open Set Metric TopologicalSpace Function Asymptotics MeasureTheory Module
   ContinuousLinearMap Filter MeasureTheory.Measure Bornology
 
 open scoped Pointwise Topology NNReal Convolution

diff --git a/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean b/Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
@@ -16,7 +16,7 @@ In this file we define `ContDiffBump.normed f μ` to be the bump function `f` no
 
 noncomputable section
 
-open Function Filter Set Metric MeasureTheory FiniteDimensional Measure
+open Function Filter Set Metric MeasureTheory Module Measure
 open scoped Topology
 
 namespace ContDiffBump

diff --git a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
@@ -24,7 +24,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddC
 
 section FiniteDimensional
 
-open Function FiniteDimensional
+open Function Module
 
 variable [CompleteSpace 𝕜]