Update Mathlib/Analysis/LocallyConvex/Basic.lean

mans0954 · j-loreaux · web-flow · commit f8148c2a35fe · 2025-03-02T09:18:58.000Z
Co-authored-by: Jireh Loreaux &lt;loreaujy@gmail.com&gt;
diff --git a/Mathlib/Analysis/LocallyConvex/Basic.lean b/Mathlib/Analysis/LocallyConvex/Basic.lean
@@ -104,7 +104,7 @@ theorem balanced_iInter₂ {f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 
   balanced_iInter fun _ => balanced_iInter <| h _
 
 theorem Balanced.mulActionHom_preimage [SMul 𝕜 F] {s : Set F} (hs : Balanced 𝕜 s)
-    (f : E →ₑ[(RingHom.id 𝕜)] F) : Balanced 𝕜 (f ⁻¹' s) := fun a ha x ⟨y,⟨hy₁,hy₂⟩⟩ => by
+    (f : E →[𝕜] F) : Balanced 𝕜 (f ⁻¹' s) := fun a ha x ⟨y,⟨hy₁,hy₂⟩⟩ => by
   rw [mem_preimage, ← hy₂, map_smul]
   exact hs a ha (smul_mem_smul_set hy₁)
 
