chore(FiniteDimensional): rename lemmas (#10188)

Rename lemmas to enable new-style dot notation or drop repeating `FiniteDimensional.finiteDimensional_*`.
Restore old names as deprecated aliases.

Archive/Imo/Imo2019Q2.lean

@@ -65,7 +65,7 @@ open scoped Affine EuclideanGeometry Real
 
 set_option linter.uppercaseLean3 false
 
-attribute [local instance] FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two
+attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 
 variable (V : Type*) (Pt : Type*)
 

Mathlib/Analysis/InnerProductSpace/Orientation.lean

@@ -157,7 +157,7 @@ open OrthonormalBasis
 protected def finOrthonormalBasis (hn : 0 < n) (h : finrank ℝ E = n) (x : Orientation ℝ E (Fin n)) :
     OrthonormalBasis (Fin n) ℝ E := by
   haveI := Fin.pos_iff_nonempty.1 hn
-  haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
+  haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
   exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).adjustToOrientation x
 #align orientation.fin_orthonormal_basis Orientation.finOrthonormalBasis
 
@@ -166,7 +166,7 @@ protected def finOrthonormalBasis (hn : 0 < n) (h : finrank ℝ E = n) (x : Orie
 theorem finOrthonormalBasis_orientation (hn : 0 < n) (h : finrank ℝ E = n)
     (x : Orientation ℝ E (Fin n)) : (x.finOrthonormalBasis hn h).toBasis.orientation = x := by
   haveI := Fin.pos_iff_nonempty.1 hn
-  haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
+  haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
   exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <|
     finCongr h).orientation_adjustToOrientation x
 #align orientation.fin_orthonormal_basis_orientation Orientation.finOrthonormalBasis_orientation
@@ -262,7 +262,7 @@ value by the product of the norms of the vectors `v i`. -/
 theorem abs_volumeForm_apply_le (v : Fin n → E) : |o.volumeForm v| ≤ ∏ i : Fin n, ‖v i‖ := by
   cases' n with n
   · refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
-  haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
+  haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
   have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
   let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
   have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
@@ -286,7 +286,7 @@ theorem abs_volumeForm_apply_of_pairwise_orthogonal {v : Fin n → E}
     (hv : Pairwise fun i j => ⟪v i, v j⟫ = 0) : |o.volumeForm v| = ∏ i : Fin n, ‖v i‖ := by
   cases' n with n
   · refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
-  haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
+  haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
   have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
   let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
   have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v
@@ -334,7 +334,7 @@ theorem volumeForm_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E)
     o.volumeForm (φ ∘ x) = o.volumeForm x := by
   cases' n with n -- Porting note: need to explicitly prove `FiniteDimensional ℝ E`
   · refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
-  haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
+  haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
   convert o.volumeForm_map φ (φ ∘ x)
   · symm
     rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -915,8 +915,8 @@ space, there exists an isometry from the orthogonal complement of a nonzero sing
 `EuclideanSpace 𝕜 (Fin n)`. -/
 def OrthonormalBasis.fromOrthogonalSpanSingleton (n : ℕ) [Fact (finrank 𝕜 E = n + 1)] {v : E}
     (hv : v ≠ 0) : OrthonormalBasis (Fin n) 𝕜 (𝕜 ∙ v)ᗮ :=
-  -- Porting note: was `attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ`
-  haveI : FiniteDimensional 𝕜 E := fact_finiteDimensional_of_finrank_eq_succ (K := 𝕜) (V := E) n
+  -- Porting note: was `attribute [local instance] FiniteDimensional.of_fact_finrank_eq_succ`
+  haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ (K := 𝕜) (V := E) n
   (stdOrthonormalBasis _ _).reindex <| finCongr <| finrank_orthogonal_span_singleton hv
 #align orthonormal_basis.from_orthogonal_span_singleton OrthonormalBasis.fromOrthogonalSpanSingleton
 

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -1173,7 +1173,7 @@ theorem Submodule.finrank_add_finrank_orthogonal' [FiniteDimensional 𝕜 E] {K
 span of a nonzero vector is one less than the dimension of the space. -/
 theorem finrank_orthogonal_span_singleton {n : ℕ} [_i : Fact (finrank 𝕜 E = n + 1)] {v : E}
     (hv : v ≠ 0) : finrank 𝕜 (𝕜 ∙ v)ᗮ = n := by
-  haveI : FiniteDimensional 𝕜 E := fact_finiteDimensional_of_finrank_eq_succ n
+  haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ n
   exact Submodule.finrank_add_finrank_orthogonal' <| by
     simp [finrank_span_singleton hv, _i.elim, add_comm]
 #align finrank_orthogonal_span_singleton finrank_orthogonal_span_singleton

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

@@ -74,11 +74,15 @@ open scoped RealInnerProductSpace ComplexConjugate
 
 open FiniteDimensional
 
-lemma FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two {K V : Type*} [DivisionRing K]
+lemma FiniteDimensional.of_fact_finrank_eq_two {K V : Type*} [DivisionRing K]
     [AddCommGroup V] [Module K V] [Fact (finrank K V = 2)] : FiniteDimensional K V :=
-  fact_finiteDimensional_of_finrank_eq_succ 1
+  .of_fact_finrank_eq_succ 1
 
-attribute [local instance] FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two
+attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
+
+@[deprecated] -- Since 2024/02/02
+alias FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two :=
+  FiniteDimensional.of_fact_finrank_eq_two
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (finrank ℝ E = 2)]
   (o : Orientation ℝ E (Fin 2))

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -33,7 +33,7 @@ linear maps are continuous. Moreover, a finite-dimensional subspace is always co
   resolution. It is however registered as an instance for `𝕜 = ℝ` and `𝕜 = ℂ`. As properness
   implies completeness, there is no need to also register `FiniteDimensional.complete` on `ℝ` or
   `ℂ`.
-* `finiteDimensional_of_isCompact_closedBall`: Riesz' theorem: if the closed unit ball is
+* `FiniteDimensional.of_isCompact_closedBall`: Riesz' theorem: if the closed unit ball is
   compact, then the space is finite-dimensional.
 
 ## Implementation notes
@@ -422,7 +422,7 @@ variable (𝕜)
 
 /-- **Riesz's theorem**: if a closed ball with center zero of positive radius is compact in a vector
 space, then the space is finite-dimensional. -/
-theorem finiteDimensional_of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
+theorem FiniteDimensional.of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
     (h : IsCompact (Metric.closedBall (0 : E) r)) : FiniteDimensional 𝕜 E := by
   by_contra hfin
   obtain ⟨R, f, Rgt, fle, lef⟩ :
@@ -452,22 +452,29 @@ theorem finiteDimensional_of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
       apply lef (ne_of_gt _)
       exact φmono (Nat.lt_succ_self N)
     _ < ‖c‖ := hN (N + 1) (Nat.le_succ N)
-#align finite_dimensional_of_is_compact_closed_ball₀ finiteDimensional_of_isCompact_closedBall₀
+#align finite_dimensional_of_is_compact_closed_ball₀ FiniteDimensional.of_isCompact_closedBall₀
+
+@[deprecated] -- Since 2024/02/02
+alias finiteDimensional_of_isCompact_closedBall₀ := FiniteDimensional.of_isCompact_closedBall₀
 
 /-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
 space is finite-dimensional. -/
-theorem finiteDimensional_of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : E}
-    (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 E := by
-  apply finiteDimensional_of_isCompact_closedBall₀ 𝕜 rpos
-  have : Continuous fun x => -c + x := continuous_const.add continuous_id
-  simpa using h.image this
-#align finite_dimensional_of_is_compact_closed_ball finiteDimensional_of_isCompact_closedBall
+theorem FiniteDimensional.of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : E}
+    (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 E :=
+  .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)
+#align finite_dimensional_of_is_compact_closed_ball FiniteDimensional.of_isCompact_closedBall
+
+@[deprecated] -- Since 2024/02/02
+alias finiteDimensional_of_isCompact_closedBall := FiniteDimensional.of_isCompact_closedBall
 
 /-- **Riesz's theorem**: a locally compact normed vector space is finite-dimensional. -/
-theorem finiteDimensional_of_locallyCompactSpace [LocallyCompactSpace E] :
-    FiniteDimensional 𝕜 E := by
-  rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
-  exact finiteDimensional_of_isCompact_closedBall₀ 𝕜 rpos hr
+theorem FiniteDimensional.of_locallyCompactSpace [LocallyCompactSpace E] :
+    FiniteDimensional 𝕜 E :=
+  let ⟨_r, rpos, hr⟩ := exists_isCompact_closedBall (0 : E)
+  .of_isCompact_closedBall₀ 𝕜 rpos hr
+
+@[deprecated] -- Since 2024/02/02
+alias finiteDimensional_of_locallyCompactSpace := FiniteDimensional.of_locallyCompactSpace
 
 /-- If a function has compact multiplicative support, then either the function is trivial or the
 space is finite-dimensional. -/
@@ -490,7 +497,7 @@ theorem HasCompactMulSupport.eq_one_or_finiteDimensional {X : Type*} [Topologica
     Metric.nhds_basis_closedBall.mem_iff.1 this
   have : IsCompact (Metric.closedBall x r) :=
     hf.of_isClosed_subset Metric.isClosed_ball (hr.trans (subset_mulTSupport _))
-  exact finiteDimensional_of_isCompact_closedBall 𝕜 rpos this
+  exact .of_isCompact_closedBall 𝕜 rpos this
 #align has_compact_mul_support.eq_one_or_finite_dimensional HasCompactMulSupport.eq_one_or_finiteDimensional
 #align has_compact_support.eq_zero_or_finite_dimensional HasCompactSupport.eq_zero_or_finiteDimensional
 
@@ -605,7 +612,7 @@ instance {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
     ProperSpace S := by
   nontriviality E
   have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
-  have : FiniteDimensional 𝕜 E := finiteDimensional_of_locallyCompactSpace 𝕜
+  have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
   exact FiniteDimensional.proper 𝕜 S
 
 /-- If `E` is a finite dimensional normed real vector space, `x : E`, and `s` is a neighborhood of
@@ -635,7 +642,7 @@ nonrec theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type*}
   · rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
     rcases hx' with ⟨r, hr₀, hrK⟩
     have : FiniteDimensional ℝ E :=
-      finiteDimensional_of_isCompact_closedBall ℝ hr₀
+      .of_isCompact_closedBall ℝ hr₀
         (hK.of_isClosed_subset Metric.isClosed_ball hrK)
     exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
   · refine' ⟨x, hx', _⟩

Mathlib/FieldTheory/KrullTopology.lean

@@ -86,7 +86,7 @@ def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgrou
 /-- For a field extension `L/K`, the intermediate field `K` is finite-dimensional over `K` -/
 theorem IntermediateField.finiteDimensional_bot (K L : Type*) [Field K] [Field L] [Algebra K L] :
     FiniteDimensional K (⊥ : IntermediateField K L) :=
-  finiteDimensional_of_rank_eq_one IntermediateField.rank_bot
+  .of_rank_eq_one IntermediateField.rank_bot
 #align intermediate_field.finite_dimensional_bot IntermediateField.finiteDimensional_bot
 
 /-- This lemma says that `Gal(L/K) = L ≃ₐ[K] L` -/

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -279,7 +279,7 @@ theorem isAlgebraic_of_finite_intermediateField
   have ⟨_m, _n, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite fun n ↦ F⟮α ^ n⟯
   isAlgebraic_of_adjoin_eq_adjoin F E hneq heq
 
-theorem finiteDimensional_of_finite_intermediateField
+theorem FiniteDimensional.of_finite_intermediateField
     [Finite (IntermediateField F E)] : FiniteDimensional F E := by
   let IF := { K : IntermediateField F E // ∃ x, K = F⟮x⟯ }
   haveI : ∀ K : IF, FiniteDimensional F K.1 := fun ⟨_, x, rfl⟩ ↦ adjoin.finiteDimensional
@@ -290,9 +290,12 @@ theorem finiteDimensional_of_finite_intermediateField
   rw [htop] at hfin
   exact topEquiv.toLinearEquiv.finiteDimensional
 
+@[deprecated] -- Since 2024/02/02
+alias finiteDimensional_of_finite_intermediateField := FiniteDimensional.of_finite_intermediateField
+
 theorem exists_primitive_element_of_finite_intermediateField
     [Finite (IntermediateField F E)] (K : IntermediateField F E) : ∃ α : E, F⟮α⟯ = K := by
-  haveI := finiteDimensional_of_finite_intermediateField F E
+  haveI := FiniteDimensional.of_finite_intermediateField F E
   rcases finite_or_infinite F with (_ | _)
   · obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K
     exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩
@@ -301,17 +304,20 @@ theorem exists_primitive_element_of_finite_intermediateField
     simp_rw [adjoin_simple_adjoin_simple, eq_comm]
     exact primitive_element_inf_aux_of_finite_intermediateField F α β
 
-theorem finiteDimensional_of_exists_primitive_element (halg : Algebra.IsAlgebraic F E)
+theorem FiniteDimensional.of_exists_primitive_element (halg : Algebra.IsAlgebraic F E)
     (h : ∃ α : E, F⟮α⟯ = ⊤) : FiniteDimensional F E := by
   obtain ⟨α, hprim⟩ := h
   have hfin := adjoin.finiteDimensional (halg α).isIntegral
   rw [hprim] at hfin
   exact topEquiv.toLinearEquiv.finiteDimensional
 
+@[deprecated] -- Since 2024/02/02
+alias finiteDimensional_of_exists_primitive_element := FiniteDimensional.of_exists_primitive_element
+
 -- A finite simple extension has only finitely many intermediate fields
 theorem finite_intermediateField_of_exists_primitive_element (halg : Algebra.IsAlgebraic F E)
     (h : ∃ α : E, F⟮α⟯ = ⊤) : Finite (IntermediateField F E) := by
-  haveI := finiteDimensional_of_exists_primitive_element F E halg h
+  haveI := FiniteDimensional.of_exists_primitive_element F E halg h
   obtain ⟨α, hprim⟩ := h
   -- Let `f` be the minimal polynomial of `α ∈ E` over `F`
   let f : F[X] := minpoly F α

Mathlib/FieldTheory/Tower.lean

@@ -78,7 +78,7 @@ theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDo
       ⟨⟨⊥, ⊤, fun he =>
           Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
     eq_bot_or_eq_top := fun K => by
-      haveI : FiniteDimensional _ _ := finiteDimensional_of_finrank hp.pos
+      haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
       letI := divisionRingOfFiniteDimensional F K
       refine' (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp _ fun h => _
       · exact Subalgebra.eq_bot_of_finrank_one

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -357,7 +357,7 @@ orthogonalization, but in the finite-dimensional case it follows more easily by
 
 -- Porting note: unnecessary in Lean 3
 private theorem findim (n : ℕ) [Fact (finrank ℝ E = n + 1)] : FiniteDimensional ℝ E :=
-  fact_finiteDimensional_of_finrank_eq_succ n
+  .of_fact_finrank_eq_succ n
 
 /-- Variant of the stereographic projection, for the sphere in an `n + 1`-dimensional inner product
 space `E`.  This version has codomain the Euclidean space of dimension `n`, and is obtained by

Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -800,7 +800,7 @@ theorem Collinear.coplanar_insert {s : Set P} (h : Collinear k s) (p : P) :
 
 /-- A set of points in a two-dimensional space is coplanar. -/
 theorem coplanar_of_finrank_eq_two (s : Set P) (h : finrank k V = 2) : Coplanar k s := by
-  have : FiniteDimensional k V := finiteDimensional_of_finrank_eq_succ h
+  have : FiniteDimensional k V := .of_finrank_eq_succ h
   rw [coplanar_iff_finrank_le_two, ← h]
   exact Submodule.finrank_le _
 #align coplanar_of_finrank_eq_two coplanar_of_finrank_eq_two