diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
index c1711ef3e96f65..e3c3d944996113 100644
--- a/Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
+++ b/Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
@@ -142,3 +142,16 @@ lemma PrimeSpectrum.comap_surjective_of_faithfullyFlat :
 @[deprecated (since := "2025-12-10")]
 alias PrimeSpectrum.specComap_surjective_of_faithfullyFlat :=
   PrimeSpectrum.comap_surjective_of_faithfullyFlat
+
+section IsLocalRing
+
+variable (A B)
+
+instance Module.FaithfullyFlat.isLocalHom : IsLocalHom (algebraMap A B) :=
+  IsLocalHom.of_comap_surjective (algebraMap A B) PrimeSpectrum.comap_surjective_of_faithfullyFlat
+
+/-- Let `B` be a faithfully flat `A`-algebra, then `A` is a local ring if `B` is. -/
+theorem Module.FaithfullyFlat.isLocalRing [IsLocalRing B] : IsLocalRing A :=
+  (algebraMap A B).domain_isLocalRing
+
+end IsLocalRing