refactor: improve API connecting ℝ- and 𝕜-linear functionals (#34543)

This PR concerns the extension of `ℝ`-linear (continuous or not) functionals to `𝕜`-linear functionals. This does several things, but I felt it was better to do it all at once, rather than having repeated churn in the same files because the current setup is a mess for numerous reasons. Unfortunately, that means the diff is a bit of a mess; I think the easiest way to review this PR is read the following discussion and then only look at the *new* code (and check that the deprecations exist).

I will begin by highlighting the current problems:

1. Naming: the primary declarations `LinearMap.extendTo𝕜'` and `ContinuousLinearMap.extendTo𝕜'` are in the wrong namespaces (`Module.Dual` and `StrongDual`), and contain a variable name `𝕜`.
2. These declarations are primed, and their unprimed counterparts operate directly on `RestrictScalars`. This is nominally (according to the module documentation) for convenience, but it leads to defeq abuse (see #34530) and so should be avoided anyway. That PR removes the only occurrence of the use of the unprimed declarations in Mathlib.
3. The declaration `ContinuousLinearMap.extendTo𝕜'` has type class assumptions (normed ones) that are too strong, thereby making it unusable for non-normed spaces (e.g., when one wants to consider continuous linear functionals on the weak dual of a Banach space).
4. Point (3) led to the creation of `RCLike.extendTo𝕜'ₗ` which is just `ContinuousLinearMap.extendTo𝕜'` except reproven with weaker type class assumptions and bundled into a linear map.
5. There are missing `simp` lemmas, namely, ones concerning the imaginary part of the extension applied to a vector.
6. We're missing appropriately bundled versions, with `RCLike.extendTo𝕜'ₗ` being the only bundling currently.

In this PR: we fix the above by doing the following:

1. Renaming `LinearMap.extendTo𝕜'` → `Module.Dual.extendRCLike` and `ContinuousLinearMap.extendTo𝕜'` → `StrongDual.extendRCLike`.
2. Removing the unprimed counterparts that operate on `RestrictScalars`
3. Weakening the type class assumptions on the newly renamed `StrongDual.extendRCLike`
4. Move `RCLike.extendTo𝕜'ₗ` out of its current location (`Analysis/LocallyConvex/Separation`) and next to `StrongDual.extendRCLike`; use the newly generalized `StrongDual.extendRCLike` to define it; rename it to `StrongDual.extendRCLikeₗ`; upgrade it from a linear map to a linear equivalence.
5. Add the missing simp lemmas for imaginary parts.
6. Add other appropriate bundlings, namely `Module.Dual.extendRCLikeₗ : Dual E ℝ ≃ₗ[ℝ] Dual E 𝕜`, and, in the context of normed spaces `StrongDual.extendRCLikeₗᵢ : StrongDual E ℝ ≃ₗᵢ[ℝ] StrongDual E 𝕜`.

Author: j-loreaux

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -210,51 +210,30 @@ end
 namespace RCLike
 
 variable [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E]
-
-/-- Real linear extension of continuous extension of `LinearMap.extendTo𝕜'` -/
-noncomputable def extendTo𝕜'ₗ [ContinuousConstSMul 𝕜 E] : StrongDual ℝ E →ₗ[ℝ] StrongDual 𝕜 E :=
-  letI to𝕜 (fr : StrongDual ℝ E) : StrongDual 𝕜 E :=
-    { toLinearMap := LinearMap.extendTo𝕜' fr
-      cont := show Continuous fun x ↦ (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) by fun_prop }
-  have h fr x : to𝕜 fr x = ((fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜)) := rfl
-  { toFun := to𝕜
-    map_add' := by intros; ext; simp [h]; ring
-    map_smul' := by intros; ext; simp [h, real_smul_eq_coe_mul]; ring }
-
-@[simp]
-lemma re_extendTo𝕜'ₗ [ContinuousConstSMul 𝕜 E] (g : StrongDual ℝ E) (x : E) :
-    re ((extendTo𝕜'ₗ g) x : 𝕜) = g x := by
-  have h g (x : E) : extendTo𝕜'ₗ g x = ((g x : 𝕜) - (I : 𝕜) * (g ((I : 𝕜) • x) : 𝕜)) := rfl
-  simp only [h, map_sub, ofReal_re, mul_re, I_re, zero_mul, ofReal_im, mul_zero,
-    sub_self, sub_zero]
-
 variable [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
 
 theorem separate_convex_open_set {s : Set E}
     (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) :
     ∃ f : StrongDual 𝕜 E, re (f x₀) = 1 ∧ ∀ x ∈ s, re (f x) < 1 := by
   have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
   obtain ⟨g, hg⟩ := _root_.separate_convex_open_set hs₀ hs₁ hs₂ hx₀
-  use extendTo𝕜'ₗ g
-  simp only [re_extendTo𝕜'ₗ]
-  exact hg
+  use g.extendRCLikeₗ
+  simpa [g.extendRCLikeₗ_apply]
 
 theorem geometric_hahn_banach_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht : Convex ℝ t)
     (disj : Disjoint s t) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧
     ∀ b ∈ t, u ≤ re (f b) := by
   have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
   obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open hs₁ hs₂ ht disj
-  use extendTo𝕜'ₗ f
-  simp only [re_extendTo𝕜'ₗ]
-  exact Exists.intro u h
+  use f.extendRCLikeₗ
+  simpa [f.extendRCLikeₗ_apply] using Exists.intro u h
 
 theorem geometric_hahn_banach_open_point (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (disj : x ∉ s) :
     ∃ f : StrongDual 𝕜 E, ∀ a ∈ s, re (f a) < re (f x) := by
   have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
   obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ disj
-  use extendTo𝕜'ₗ f
-  simp only [re_extendTo𝕜'ₗ]
-  exact fun a a_1 ↦ h a a_1
+  use f.extendRCLikeₗ
+  simpa [f.extendRCLikeₗ_apply]
 
 theorem geometric_hahn_banach_point_open (ht₁ : Convex ℝ t) (ht₂ : IsOpen t) (disj : x ∉ t) :
     ∃ f : StrongDual 𝕜 E, ∀ b ∈ t, re (f x) < re (f b) :=
@@ -266,9 +245,8 @@ theorem geometric_hahn_banach_open_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s
     ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u < re (f b) := by
   have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
   obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open_open hs₁ hs₂ ht₁ ht₃ disj
-  use extendTo𝕜'ₗ f
-  simp only [re_extendTo𝕜'ₗ]
-  exact Exists.intro u h
+  use f.extendRCLikeₗ
+  simpa [f.extendRCLikeₗ_apply] using Exists.intro u h
 
 variable [LocallyConvexSpace ℝ E]
 
@@ -277,9 +255,8 @@ theorem geometric_hahn_banach_compact_closed (hs₁ : Convex ℝ s) (hs₂ : IsC
     ∃ (f : StrongDual 𝕜 E) (u v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b) := by
   have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
   obtain ⟨g, u, v, h1⟩ := _root_.geometric_hahn_banach_compact_closed hs₁ hs₂ ht₁ ht₂ disj
-  use extendTo𝕜'ₗ g
-  simp only [re_extendTo𝕜'ₗ, exists_and_left]
-  exact ⟨u, h1.1, v, h1.2⟩
+  use g.extendRCLikeₗ
+  simpa [g.extendRCLikeₗ_apply, exists_and_left] using ⟨u, h1.1, v, h1.2⟩
 
 theorem geometric_hahn_banach_closed_compact (hs₁ : Convex ℝ s) (hs₂ : IsClosed s)
     (ht₁ : Convex ℝ t) (ht₂ : IsCompact t) (disj : Disjoint s t) :

Mathlib/Analysis/Normed/Module/HahnBanach.lean

@@ -87,21 +87,21 @@ theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : StrongDual 𝕜 p) :
   obtain ⟨g, ⟨(hextends : ∀ x : p, g x = fr x), hnormeq⟩⟩ :=
     Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr
   -- Now `g` can be extended to the `StrongDual 𝕜 E` we need.
-  refine ⟨g.extendTo𝕜', ?_⟩
+  refine ⟨g.extendRCLike, ?_⟩
   -- It is an extension of `f`.
-  have h (x : p) : g.extendTo𝕜' x = f x := by
-    rw [ContinuousLinearMap.extendTo𝕜'_apply, ← Submodule.coe_smul,
+  have h (x : p) : g.extendRCLike x = f x := by
+    rw [g.extendRCLike_apply, ← Submodule.coe_smul,
       hextends, hextends]
     simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]
   -- And we derive the equality of the norms by bounding on both sides.
   refine ⟨h, le_antisymm ?_ ?_⟩
   · calc
-      ‖g.extendTo𝕜'‖ = ‖g‖ := g.norm_extendTo𝕜'
+      ‖g.extendRCLike‖ = ‖g‖ := g.norm_extendRCLike
       _ = ‖fr‖ := hnormeq
       _ ≤ ‖reCLM‖ * ‖f‖ := ContinuousLinearMap.opNorm_comp_le _ _
       _ = ‖f‖ := by rw [reCLM_norm, one_mul]
-  · exact f.opNorm_le_bound (g.extendTo𝕜' (𝕜 := 𝕜)).opNorm_nonneg
-      fun x ↦ h x ▸ (g.extendTo𝕜' (𝕜 := 𝕜) |>.le_opNorm x)
+  · exact f.opNorm_le_bound (g.extendRCLike (𝕜 := 𝕜)).opNorm_nonneg
+      fun x ↦ h x ▸ (g.extendRCLike (𝕜 := 𝕜) |>.le_opNorm x)
 
 open Module
 

Mathlib/Analysis/Normed/Module/RCLike/Extend.lean

@@ -11,51 +11,56 @@ public import Mathlib.Analysis.Normed.Operator.Basic
 /-!
 # Norm properties of the extension of continuous `ℝ`-linear functionals to `𝕜`-linear functionals
 
-This file shows that `ContinuousLinearMap.extendTo𝕜` preserves the norm of the functional.
+This file shows that `StrongDual.extendRCLike` preserves the norm of the functional.
 -/
 
 public section
 
-open RCLike
+open RCLike ContinuousLinearMap
 open scoped ComplexConjugate
 
-namespace ContinuousLinearMap
-
-variable {𝕜 F : Type*} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+namespace StrongDual
 
-section ScalarTower
 
+variable {𝕜 F : Type*} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
 variable [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F]
 
 /-- The norm of the extension is bounded by `‖fr‖`. -/
-theorem norm_extendTo𝕜'_bound (fr : StrongDual ℝ F) (x : F) :
-    ‖(fr.extendTo𝕜' x : 𝕜)‖ ≤ ‖fr‖ * ‖x‖ := by
-  set lm : F →L[𝕜] 𝕜 := fr.extendTo𝕜'
+theorem norm_extendRCLike_bound (fr : StrongDual ℝ F) (x : F) :
+    ‖(fr.extendRCLike x : 𝕜)‖ ≤ ‖fr‖ * ‖x‖ := by
+  set lm : StrongDual 𝕜 F := fr.extendRCLike
   by_cases h : lm x = 0
   · rw [h, norm_zero]
     positivity
   rw [← mul_le_mul_iff_right₀ (norm_pos_iff.2 h), ← sq]
   calc
-    ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := fr.toLinearMap.norm_extendTo𝕜'_apply_sq x
+    ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := Module.Dual.norm_extendRCLike_apply_sq fr.toLinearMap x
     _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := le_abs_self _
     _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := le_opNorm _ _
     _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]
 
 @[simp]
-theorem norm_extendTo𝕜' (fr : StrongDual ℝ F) : ‖(fr.extendTo𝕜' : StrongDual 𝕜 F)‖ = ‖fr‖ :=
-  le_antisymm (ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fr.norm_extendTo𝕜'_bound) <|
+theorem norm_extendRCLike (fr : StrongDual ℝ F) : ‖(fr.extendRCLike : StrongDual 𝕜 F)‖ = ‖fr‖ :=
+  le_antisymm (ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fr.norm_extendRCLike_bound) <|
     opNorm_le_bound _ (norm_nonneg _) fun x =>
       calc
-        ‖fr x‖ = ‖re (fr.extendTo𝕜' x : 𝕜)‖ := congr_arg norm (fr.extendTo𝕜'_apply_re x).symm
-        _ ≤ ‖(fr.extendTo𝕜' x : 𝕜)‖ := abs_re_le_norm _
-        _ ≤ ‖(fr.extendTo𝕜' : StrongDual 𝕜 F)‖ * ‖x‖ := le_opNorm _ _
+        ‖fr x‖ = ‖re (fr.extendRCLike x : 𝕜)‖ := by simp
+        _ ≤ ‖(fr.extendRCLike x : 𝕜)‖ := abs_re_le_norm _
+        _ ≤ ‖(fr.extendRCLike : StrongDual 𝕜 F)‖ * ‖x‖ := le_opNorm _ _
 
-end ScalarTower
+/-- `StrongDual.extendRCLike` bundled into a linear isometry equivalence. -/
+@[expose, simps! -isSimp apply symm_apply]
+noncomputable def extendRCLikeₗᵢ : StrongDual ℝ F ≃ₗᵢ[ℝ] StrongDual 𝕜 F where
+  toLinearEquiv := StrongDual.extendRCLikeₗ
+  norm_map' := norm_extendRCLike
 
-set_option backward.isDefEq.respectTransparency false in
-@[simp]
-theorem norm_extendTo𝕜 (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) :
-    ‖fr.extendTo𝕜‖ = ‖fr‖ :=
-  fr.norm_extendTo𝕜'
+end StrongDual
+
+namespace ContinuousLinearMap
+open StrongDual
+
+@[deprecated (since := "2026-02-24")] alias norm_extendTo𝕜'_bound := norm_extendRCLike_bound
+@[deprecated (since := "2026-02-24")] alias norm_extendTo𝕜' := norm_extendRCLike
+@[deprecated (since := "2026-02-24")] alias norm_extendTo𝕜 := norm_extendRCLike
 
 end ContinuousLinearMap

Mathlib/Analysis/RCLike/Extend.lean

@@ -26,35 +26,25 @@ elementary properties, like locally convex spaces.
 
 ## Main definitions
 
-* `LinearMap.extendTo𝕜`
-* `ContinuousLinearMap.extendTo𝕜`
-
-## Implementation details
-
-For convenience, the main definitions above operate in terms of `RestrictScalars ℝ 𝕜 F`.
-Alternate forms which operate on `[IsScalarTower ℝ 𝕜 F]` instead are provided with a primed name.
+* `LinearMap.extendRCLike`
+* `ContinuousLinearMap.extendRCLike`
 
 -/
 
 @[expose] public section
 
-
 open RCLike
 
 open ComplexConjugate
 
 variable {𝕜 : Type*} [RCLike 𝕜] {F : Type*}
-namespace LinearMap
-
-open Module
-
-section ScalarTower
+namespace Module.Dual
 
 variable [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F]
 
 /-- Extend `fr : Dual ℝ F` to `Dual 𝕜 F` in a way that will also be continuous and have its norm
 (as a continuous linear map) equal to `‖fr‖` when `fr` is itself continuous on a normed space. -/
-noncomputable def extendTo𝕜' (fr : Dual ℝ F) : Dual 𝕜 F :=
+noncomputable def extendRCLike (fr : Dual ℝ F) : Dual 𝕜 F :=
   letI fc : F → 𝕜 := fun x => (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x)
   have add (x y) : fc (x + y) = fc x + fc y := by
     simp only [fc, smul_add, map_add, mul_add]
@@ -73,69 +63,107 @@ noncomputable def extendTo𝕜' (fr : Dual ℝ F) : Dual 𝕜 F :=
     map_add' := add
     map_smul' := smul_𝕜 }
 
-theorem extendTo𝕜'_apply (fr : Dual ℝ F) (x : F) :
-    fr.extendTo𝕜' x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
+theorem extendRCLike_apply (fr : Dual ℝ F) (x : F) :
+    fr.extendRCLike x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
 
 @[simp]
-theorem extendTo𝕜'_apply_re (fr : Dual ℝ F) (x : F) : re (fr.extendTo𝕜' x : 𝕜) = fr x := by
-  simp only [extendTo𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero, rclike_simps]
+theorem re_extendRCLike_apply (fr : Dual ℝ F) (x : F) : re (fr.extendRCLike x : 𝕜) = fr x := by
+  simp only [extendRCLike_apply, map_sub, zero_mul, mul_zero, sub_zero, rclike_simps]
 
-theorem norm_extendTo𝕜'_apply_sq (fr : Dual ℝ F) (x : F) :
-    ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = fr (conj (fr.extendTo𝕜' x : 𝕜) • x) := calc
-  ‖(fr.extendTo𝕜' x : 𝕜)‖ ^ 2 = re (conj (fr.extendTo𝕜' x) * fr.extendTo𝕜' x : 𝕜) := by
+@[simp]
+lemma im_extendRCLike_apply (g : Dual ℝ F) (x : F) :
+    im ((extendRCLike g) x : 𝕜) = - g ((I : 𝕜) • x) := by
+  obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
+  all_goals simp [h, extendRCLike_apply]
+
+theorem norm_extendRCLike_apply_sq (fr : Dual ℝ F) (x : F) :
+    ‖(fr.extendRCLike x : 𝕜)‖ ^ 2 = fr (conj (fr.extendRCLike x : 𝕜) • x) := calc
+  ‖(fr.extendRCLike x : 𝕜)‖ ^ 2 = re (conj (fr.extendRCLike x) * fr.extendRCLike x : 𝕜) := by
     rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]
-  _ = fr (conj (fr.extendTo𝕜' x : 𝕜) • x) := by
-    rw [← smul_eq_mul, ← map_smul, extendTo𝕜'_apply_re]
+  _ = fr (conj (fr.extendRCLike x : 𝕜) • x) := by
+    rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]
 
-end ScalarTower
+/-- The extension `Module.Dual.extendRCLike` as a linear equivalence between the algebraic duals. -/
+@[simps -isSimp apply symm_apply]
+noncomputable def extendRCLikeₗ : Dual ℝ F ≃ₗ[ℝ] Dual 𝕜 F where
+  toFun := extendRCLike (𝕜 := 𝕜)
+  invFun f := RCLike.reLm.comp (f.restrictScalars ℝ)
+  left_inv f := by ext; simp
+  right_inv f := by ext; apply RCLike.ext <;> simp
+  map_add' := by intros; ext; simp [extendRCLike_apply]; ring
+  map_smul' := by intros; ext; simp [extendRCLike_apply, real_smul_eq_coe_mul]; ring
 
-section RestrictScalars
+end Module.Dual
 
-variable [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+namespace StrongDual
 
-instance : NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F) :=
-  inferInstanceAs (NormedSpace 𝕜 F)
+variable [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F]
+variable [Module ℝ F] [IsScalarTower ℝ 𝕜 F]
 
-/-- Extend `fr : Dual ℝ (RestrictScalars ℝ 𝕜 F)` to `Dual 𝕜 F`. -/
-noncomputable def extendTo𝕜 (fr : Dual ℝ (RestrictScalars ℝ 𝕜 F)) : Dual 𝕜 F :=
-  fr.extendTo𝕜'
+/-- Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.
 
-theorem extendTo𝕜_apply (fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ) (x : F) :
-    fr.extendTo𝕜 x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
+It would be possible to use `LinearMap.mkContinuous` here, but we would need to know that the
+continuity of `fr` implies it has bounded norm and we want to avoid that dependency here.
 
-end RestrictScalars
+Norm properties of this extension can be found in
+`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`. -/
+noncomputable def extendRCLike (fr : StrongDual ℝ F) : StrongDual 𝕜 F where
+  __ := Module.Dual.extendRCLike fr.toLinearMap
+  cont := show Continuous fun x ↦ (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) by fun_prop
 
-end LinearMap
+theorem extendRCLike_apply (fr : StrongDual ℝ F) (x : F) :
+    fr.extendRCLike x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
 
-namespace ContinuousLinearMap
+@[simp]
+lemma re_extendRCLike_apply (g : StrongDual ℝ F) (x : F) :
+    re ((extendRCLike g) x : 𝕜) = g x := by
+  simp [extendRCLike_apply]
 
-variable [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+@[deprecated (since := "2026-02-24")] alias _root_.RCLike.re_extendTo𝕜ₗ := re_extendRCLike_apply
 
-section ScalarTower
+@[simp]
+lemma im_extendRCLike_apply (g : StrongDual ℝ F) (x : F) :
+    im ((extendRCLike g) x : 𝕜) = - g ((I : 𝕜) • x) := by
+  obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
+  all_goals simp [h, extendRCLike_apply]
 
-variable [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F]
+/-- The extension `StrongDual.extendRCLike` as a linear equivalence between the algebraic duals.
 
-/-- Extend `fr : StrongDual ℝ F` to `StrongDual 𝕜 F`.
+When `F` is a normed space, this can be upgraded to an *isometric* linear equivalence, see
+`StrondDual.extendRCLikeₗᵢ`. -/
+@[simps -isSimp apply symm_apply]
+noncomputable def extendRCLikeₗ : StrongDual ℝ F ≃ₗ[ℝ] StrongDual 𝕜 F where
+  toFun := StrongDual.extendRCLike (𝕜 := 𝕜)
+  invFun f := RCLike.reCLM.comp (f.restrictScalars ℝ)
+  left_inv f := by ext; simp
+  right_inv f := by ext; apply RCLike.ext <;> simp [extendRCLike_apply]
+  map_add' := by intros; ext; simp [extendRCLike_apply]; ring
+  map_smul' := by intros; ext; simp [extendRCLike_apply, real_smul_eq_coe_mul]; ring
 
-It would be possible to use `LinearMap.mkContinuous` here, but we would need to know that the
-continuity of `fr` implies it has bounded norm and we want to avoid that dependency here.
+@[deprecated (since := "2026-02-24")] alias _root_.RCLike.extendTo𝕜ₗ := extendRCLikeₗ
 
-Norm properties of this extension can be found in
-`Mathlib/Analysis/Normed/Module/RCLike/Extend.lean`. -/
-noncomputable def extendTo𝕜' (fr : StrongDual ℝ F) : StrongDual 𝕜 F where
-  __ := fr.toLinearMap.extendTo𝕜'
-  cont := show Continuous fun x ↦ (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) by fun_prop
+end StrongDual
+
+namespace LinearMap
+
+open Module.Dual
 
-theorem extendTo𝕜'_apply (fr : StrongDual ℝ F) (x : F) :
-    fr.extendTo𝕜' x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜' := extendRCLike
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜'_apply := extendRCLike_apply
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜'_apply_re := re_extendRCLike_apply
+@[deprecated (since := "2026-02-24")] alias norm_extendTo𝕜'_apply_sq := norm_extendRCLike_apply_sq
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜 := extendRCLike
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜_apply := extendRCLike_apply
 
-end ScalarTower
+end LinearMap
+
+namespace ContinuousLinearMap
 
-/-- Extend `fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)` to `StrongDual 𝕜 F`. -/
-noncomputable def extendTo𝕜 (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) :
-    StrongDual 𝕜 F := fr.extendTo𝕜'
+open StrongDual
 
-theorem extendTo𝕜_apply (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) (x : F) :
-    fr.extendTo𝕜 x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) := rfl
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜' := extendRCLike
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜'_apply := extendRCLike_apply
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜 := extendRCLike
+@[deprecated (since := "2026-02-24")] alias extendTo𝕜_apply := extendRCLike_apply
 
 end ContinuousLinearMap