chore: rename FiniteDimensional.of_fintype_basis (#31543)

The lemma has a Finite hypothesis now, not a Fintype one. The new name was discussed on zulip:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20convention/near/555088215

Author: grunweg

Archive/Sensitivity.lean

@@ -248,7 +248,7 @@ theorem dim_V : Module.rank ℝ (V n) = 2 ^ n := by
 
 open Classical in
 instance : FiniteDimensional ℝ (V n) :=
-  FiniteDimensional.of_fintype_basis (dualBases_e_ε _).basis
+  (dualBases_e_ε _).basis.finiteDimensional_of_finite
 
 theorem finrank_V : finrank ℝ (V n) = 2 ^ n := by
   have := @dim_V n

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -332,7 +332,7 @@ theorem setFinite_inter [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.
 theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] :
     MeasurableSet (fundamentalDomain b) := by
   cases nonempty_fintype ι
-  haveI : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
+  haveI : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
   let D : Set (ι → ℝ) := Set.pi Set.univ fun _ : ι => Set.Ico (0 : ℝ) 1
   rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]
   · refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_
@@ -365,7 +365,7 @@ theorem measure_fundamentalDomain_ne_zero [Finite ι] [MeasurableSpace E] [Borel
 theorem measure_fundamentalDomain [Fintype ι] [DecidableEq ι] [MeasurableSpace E] (μ : Measure E)
     [BorelSpace E] [Measure.IsAddHaarMeasure μ] (b₀ : Basis ι ℝ E) :
     μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det b| * μ (fundamentalDomain b₀) := by
-  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
+  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
   convert μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)
   · rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
       Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
@@ -394,7 +394,7 @@ theorem fundamentalDomain_ae_parallelepiped [Fintype ι] [MeasurableSpace E] (μ
     [BorelSpace E] [Measure.IsAddHaarMeasure μ] :
     fundamentalDomain b =ᵐ[μ] parallelepiped b := by
   classical
-  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
+  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
   rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
   suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
       AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -151,7 +151,7 @@ theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E =
   -- TODO: this could be easier with `det_cases`
   by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)
   · rcases h with ⟨s, ⟨b⟩⟩
-    haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis b
+    haveI : FiniteDimensional 𝕜 E := b.finiteDimensional_of_finite
     classical
     simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
     refine Continuous.matrix_det ?_

Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -771,7 +771,7 @@ variable [DivisionRing k] [Module k V]
 
 protected theorem finiteDimensional [Finite ι] (b : AffineBasis ι k P) : FiniteDimensional k V :=
   let ⟨i⟩ := b.nonempty
-  FiniteDimensional.of_fintype_basis (b.basisOf i)
+  (b.basisOf i).finiteDimensional_of_finite
 
 protected theorem finite [FiniteDimensional k V] (b : AffineBasis ι k P) : Finite ι :=
   finite_of_fin_dim_affineIndependent k b.ind

Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

@@ -115,7 +115,7 @@ lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι]
     B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range b))) =
       Submodule.span R (Set.range b) := by
   classical
-  letI := FiniteDimensional.of_fintype_basis b
+  letI := b.finiteDimensional_of_finite
   rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
     dualBasis_dualBasis_flip hB]
 
@@ -124,7 +124,7 @@ lemma dualSubmodule_flip_dualSubmodule_of_basis {ι : Type*} [Finite ι]
     B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) =
       Submodule.span R (Set.range b) := by
   classical
-  letI := FiniteDimensional.of_fintype_basis b
+  letI := b.finiteDimensional_of_finite
   rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
     dualBasis_flip_dualBasis hB]
 
@@ -133,7 +133,7 @@ lemma dualSubmodule_dualSubmodule_of_basis
     B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) =
       Submodule.span R (Set.range b) := by
   classical
-  letI := FiniteDimensional.of_fintype_basis b
+  letI := b.finiteDimensional_of_finite
   rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
     dualBasis_dualBasis hB hB']
 

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -371,21 +371,21 @@ variable {ι : Type*} [DecidableEq ι] [Finite ι]
 where `B` is a nondegenerate (symmetric) bilinear form and `b` is a finite basis. -/
 noncomputable def dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) :
     Basis ι K V :=
-  haveI := FiniteDimensional.of_fintype_basis b
+  haveI := b.finiteDimensional_of_finite
   b.dualBasis.map (B.toDual hB).symm
 
 variable {B : BilinForm K V}
 
 @[simp]
 theorem dualBasis_repr_apply (hB : B.Nondegenerate) (b : Basis ι K V) (x i) :
     (B.dualBasis hB b).repr x i = B x (b i) := by
-  have := FiniteDimensional.of_fintype_basis b
+  have := b.finiteDimensional_of_finite
   rw [dualBasis, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
     Basis.dualBasis_repr, toDual_def]
 
 theorem apply_dualBasis_left (hB : B.Nondegenerate) (b : Basis ι K V) (i j) :
     B (B.dualBasis hB b i) (b j) = if j = i then 1 else 0 := by
-  have := FiniteDimensional.of_fintype_basis b
+  have := b.finiteDimensional_of_finite
   rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
     LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]
 

Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean

@@ -20,7 +20,7 @@ open Module
 
 namespace Complex
 
-instance : FiniteDimensional ℝ ℂ := .of_fintype_basis basisOneI
+instance : FiniteDimensional ℝ ℂ := basisOneI.finiteDimensional_of_finite
 
 /-- `ℂ` is a finite extension of `ℝ` of degree 2, i.e `[ℂ : ℝ] = 2` -/
 @[simp, stacks 09G4]

Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

@@ -32,7 +32,7 @@ that all these points of view are equivalent, with the following lemmas
   is `Fin` (in `Mathlib/LinearAlgebra/Dimension/Free.lean`)
 - `fintypeBasisIndex` states that a finite-dimensional
   vector space has a finite basis
-- `of_fintype_basis` states that the existence of a basis indexed by a
+- `Module.Basis.finiteDimensional_of_finite` states that the existence of a basis indexed by a
   finite type implies finite-dimensionality
 - `of_finite_basis` states that the existence of a basis indexed by a
   finite set implies finite-dimensionality
@@ -66,7 +66,7 @@ universe u v v' w
 open Cardinal Module Submodule
 
 /-- `FiniteDimensional` vector spaces are defined to be finite modules.
-Use `FiniteDimensional.of_fintype_basis` to prove finite dimension from another definition. -/
+Use `Module.Basis.finiteDimensional_of_finite` to prove finite dimension from another definition. -/
 abbrev FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] :=
   Module.Finite K V
 
@@ -98,9 +98,13 @@ instance finiteDimensional_pi' {ι : Type*} [Finite ι] (M : ι → Type*) [∀
 variable {K V}
 
 /-- If a vector space has a finite basis, then it is finite-dimensional. -/
-theorem of_fintype_basis {ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V :=
+theorem _root_.Module.Basis.finiteDimensional_of_finite {ι : Type w} [Finite ι] (h : Basis ι K V) :
+    FiniteDimensional K V :=
   Module.Finite.of_basis h
 
+@[deprecated (since := "2025-11-12")]
+alias of_fintype_basis := Module.Basis.finiteDimensional_of_finite
+
 /-- If a vector space is `FiniteDimensional`, all bases are indexed by a finite type -/
 noncomputable def fintypeBasisIndex {ι : Type*} [FiniteDimensional K V] (b : Basis ι K V) :
     Fintype ι :=
@@ -116,7 +120,7 @@ finite-dimensional. -/
 theorem of_finite_basis {ι : Type w} {s : Set ι} (h : Basis s K V) (hs : Set.Finite s) :
     FiniteDimensional K V :=
   haveI := hs.fintype
-  of_fintype_basis h
+  h.finiteDimensional_of_finite
 
 /-- A subspace of a finite-dimensional space is also finite-dimensional.
 

Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

@@ -242,7 +242,7 @@ private lemma restrictScalars_field_aux
   obtain ⟨n, -, b', -⟩ := p.exists_basis_basis_of_span_eq_top_of_mem_algebraMap _ _ hM hN <| by
     rintro - ⟨m, rfl⟩ - ⟨n, rfl⟩
     exact hp m n
-  have : FiniteDimensional K (LinearMap.range i) := FiniteDimensional.of_fintype_basis b'
+  have : FiniteDimensional K (LinearMap.range i) := b'.finiteDimensional_of_finite
   exact Finite.equiv (LinearEquiv.ofInjective i hi).symm
 
 include hi hj in

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

@@ -207,9 +207,9 @@ theorem parallelepiped_reindex (b : Basis ι ℝ E) (e : ι ≃ ι') :
 
 theorem parallelepiped_map (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
     (b.map e).parallelepiped = b.parallelepiped.map e
-    (haveI := FiniteDimensional.of_fintype_basis b
+    (haveI := b.finiteDimensional_of_finite
     LinearMap.continuous_of_finiteDimensional e.toLinearMap)
-    (haveI := FiniteDimensional.of_fintype_basis (b.map e)
+    (haveI := (b.map e).finiteDimensional_of_finite
     LinearMap.isOpenMap_of_finiteDimensional _ e.surjective) :=
   PositiveCompacts.ext (image_parallelepiped e.toLinearMap _).symm
 
@@ -254,7 +254,7 @@ instance _root_.isAddHaarMeasure_basis_addHaar (b : Basis ι ℝ E) : IsAddHaarM
   rw [Basis.addHaar]; exact Measure.isAddHaarMeasure_addHaarMeasure _
 
 instance (b : Basis ι ℝ E) : SigmaFinite b.addHaar := by
-  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
+  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
   rw [Basis.addHaar_def]; exact sigmaFinite_addHaarMeasure
 
 /-- Let `μ` be a σ-finite left invariant measure on `E`. Then `μ` is equal to the Haar measure
@@ -277,8 +277,8 @@ variable [MeasurableSpace F] [BorelSpace F] [SecondCountableTopologyEither E F]
 
 theorem prod_addHaar (v : Basis ι ℝ E) (w : Basis ι' ℝ F) :
     (v.prod w).addHaar = v.addHaar.prod w.addHaar := by
-  have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis v
-  have : FiniteDimensional ℝ F := FiniteDimensional.of_fintype_basis w
+  have : FiniteDimensional ℝ E := v.finiteDimensional_of_finite
+  have : FiniteDimensional ℝ F := w.finiteDimensional_of_finite
   simp [(v.prod w).addHaar_eq_iff, Basis.prod_parallelepiped, Basis.addHaar_self]
 
 end Module.Basis