fix(AlgebraicGeometry/Modules/Tilde): remove duplicate namespace (leanprover-community#40213)

The Scheme.Modules namespace was duplicated in the declaration.
Found by the strengthening the `dupNamespace` linter in leanprover-community#39793.

Author: grunweg

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -121,12 +121,12 @@ lemma isSMulRegular_of_le_basicOpen {f : R} (hle : U ≤ PrimeSpectrum.basicOpen
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S)
+lemma restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S)
     [IsOpenImmersion (Spec.map f)] {U : (Spec S).Opens} (r : R)
     (x : Γ(M.restrict (Spec.map f), U)) :
     dsimp% (M.restrictAppIso (Spec.map f) U).hom (f r • x) =
       r • (M.restrictAppIso (Spec.map f) U).hom x := by
-  rw [Scheme.Modules.smul_Spec_def, Scheme.Modules.smul_Spec_def]
+  rw [smul_Spec_def, smul_Spec_def]
   simp_rw [smul_restrictAppIso_hom_apply, ← ConcreteCategory.comp_apply, Category.assoc]
   have :
       f ≫ (ΓSpecIso S).inv ≫ (Spec S).presheaf.map U.leTop.op ≫ (Hom.appIso (Spec.map f) U).inv =
@@ -135,6 +135,10 @@ lemma Scheme.Modules.restrictAppIso_smul_Spec {S : CommRingCat.{u}} (f : R ⟶ S
     rfl
   rw [this]
 
+set_option linter.dupNamespace false in
+@[deprecated (since := "2026-06-04")]
+alias Scheme.Modules.restrictAppIso_smul_Spec := restrictAppIso_smul_Spec
+
 end Scheme.Modules
 
 /--