diff --git a/Mathlib.lean b/Mathlib.lean
index 4126812cdba773..520afc53f608ae 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6512,6 +6512,7 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
+public import Mathlib.RingTheory.LocalRing.Etale
 public import Mathlib.RingTheory.LocalRing.Length
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
new file mode 100644
index 00000000000000..5790dfac6ef677
--- /dev/null
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 University of Washington Math AI Lab. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
+-/
+
+module
+
+public import Mathlib.RingTheory.IsAdjoinRoot
+public import Mathlib.RingTheory.LocalRing.Quotient
+public import Mathlib.RingTheory.Smooth.Flat
+public import Mathlib.RingTheory.Unramified.LocalRing
+
+/-!
+# Étale extensions of local rings
+
+We prove that a finite étale extension of local rings is monogenic (generated by a single element),
+and that the derivative of the minimal polynomial evaluated at the generator is a unit.
+These are parts 1 and 2 of Lemma 3.2 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
+
+## Main results
+
+* `IsLocalRing.exists_adjoin_eq_top`: a finite étale extension of local rings is generated by a
+  single element (Lemma 3.2, part 1).
+* `IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top`: if `R → S` is étale and
+  `R[β] = S`, then `f'(β)` is a unit, where `f = minpoly R β` (Lemma 3.2, part 2).
+
+## Key intermediate results
+
+* `IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top`: `β` generates `S` over `R` iff
+  `β mod m_S` generates `S/m_S` over `R/m_R`.
+* `IsLocalRing.finrank_eq_finrank_residueField`: for finite étale extensions of local rings,
+  `finrank R S = finrank (ResidueField R) (ResidueField S)`.
+* `IsLocalRing.minpoly_map_residue`: the minimal polynomial of `β` over `R` maps to the
+  minimal polynomial of `β mod m_S` over the residue field.
+
+## Future work
+
+The following results from [arXiv:2503.07846](https://arxiv.org/abs/2503.07846) (formalized at [uw-math-ai/monogenic-extensions](https://github.com/uw-math-ai/monogenic-extensions)) are planned for
+future PRs:
+
+* **Converse**: If `S ≅ R[X]/(f)` with `f` monic and `f'(root)` a unit, then `R → S` is étale.
+* **Lemma 3.1** (partial étale case): If `R` and `S` are local integral domains with `R`
+  integrally closed, `S` a UFD, `R → S` finite and injective, and there exists a height-one
+  prime `q ⊆ S` such that `R/(q ∩ R) → S/q` is étale, then `S ≅ R[X]/(f)` for some monic `f`.
+
+## Tags
+
+étale, monogenic, local ring, minimal polynomial, residue field
+-/
+
+@[expose] public section
+
+namespace IsLocalRing
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+    [IsLocalRing S] [IsLocalRing R] [Module.Finite R S] [FaithfulSMul R S]
+
+open Polynomial IsLocalRing Algebra
+
+/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
+generates `S/m_S` over `R/m_R`. -/
+lemma adjoin_residue_eq_top_iff_adjoin_eq_top [Algebra.Etale R S] (β : S) :
+    Algebra.adjoin (ResidueField R) {residue S β} = ⊤ ↔ Algebra.adjoin R {β} = ⊤ := by
+  constructor
+  · intro hβ
+    refine eq_top_iff.mpr <| Submodule.le_of_le_smul_of_le_jacobson_bot
+      (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥)
+      (?_ : ⊤ ≤ (adjoin R {β}).toSubmodule ⊔ maximalIdeal R • ⊤)
+    intro s _
+    rw [adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hβ
+    obtain ⟨p, hp⟩ := hβ (residue S s)
+    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ residue_surjective p
+    rw [Ideal.smul_top_eq_map]
+    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
+    · rw [adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
+    · rw [Algebra.FormallyUnramified.map_maximalIdeal]
+      erw [← Ideal.Quotient.eq,
+        map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl, hp]
+      rfl
+  · intro hβ_gen
+    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+    intro x
+    obtain ⟨s, rfl⟩ := IsLocalRing.residue_surjective (R := S) x
+    obtain ⟨p, rfl⟩ := hβ_gen s
+    exact ⟨p.map (residue R), by
+      rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]⟩
+
+/-- A finite étale extension of local rings is generated by a single element.
+This is Lemma 3.2, part 1 of [arXiv:2503.07846](https://arxiv.org/abs/2503.07846).
+The proof lifts a primitive element of the residue field extension via Nakayama's lemma. -/
+theorem exists_adjoin_eq_top [Algebra.Etale R S] :
+    ∃ β : S, Algebra.adjoin R {β} = ⊤ := by
+  obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (ResidueField R) (ResidueField S)
+  obtain ⟨β, hβ⟩ := residue_surjective (R := S) β₀
+  refine ⟨β, adjoin_residue_eq_top_iff_adjoin_eq_top β |>.mp ?_⟩
+  rw [hβ,
+    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
+    hβ₀, IntermediateField.top_toSubalgebra]
+
+/-- For finite étale extensions of local rings,
+`finrank R S = finrank (ResidueField R) (ResidueField S)`. -/
+lemma finrank_eq_finrank_residueField [Algebra.Etale R S] :
+    Module.finrank R S =
+      Module.finrank (ResidueField R) (ResidueField S) := by
+  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+  have e := AddEquiv.toLinearEquiv (R := R ⧸ maximalIdeal R) (Ideal.quotEquivOfEq <|
+      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv
+    ?_
+  · erw [← e.finrank_eq, finrank_quotient_map (R := R) (S := S)]
+  · intro r x
+    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
+    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+    simp only [RingEquiv.toAddEquiv_eq_coe]; rfl
+
+/-- For a monogenic étale extension of local rings, the minimal polynomial of `β`
+maps to the minimal polynomial of `β mod m_S` over the residue field. -/
+lemma minpoly_map_residue [Algebra.Etale R S]
+    {β : S} (hadj : Algebra.adjoin R {β} = ⊤) :
+    (minpoly R β).map (residue R) = minpoly (ResidueField R) (residue S β) := by
+  have h := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
+  -- Both monic, same degree, divisibility ⟹ equal
+  refine eq_of_monic_of_dvd_of_natDegree_le
+    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
+    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_
+  · rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
+    simp
+  · haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+    have hβ₀ := (adjoin_residue_eq_top_iff_adjoin_eq_top β).mpr hadj
+    rw [h.natDegree_map _,
+      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
+      finrank_eq_finrank_residueField,
+      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]
+
+/-- If `R → S` is étale and `R[β] = S`, then `f'(β)` is a unit in `S`,
+where `f = minpoly R β`. The proof reduces to separability of the
+residue field extension via `minpoly_map_residue`. -/
+lemma isUnit_aeval_derivative_minpoly_of_adjoin_eq_top
+    [Algebra.Etale R S] {β : S}
+    (hadj : Algebra.adjoin R {β} = ⊤) :
+    IsUnit (aeval β (minpoly R β).derivative) := by
+  apply fun s => (residue_ne_zero_iff_isUnit s).mp
+  rw [map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl,
+    ← derivative_map, minpoly_map_residue hadj]
+  exact Algebra.IsSeparable.isSeparable _ _ |>.aeval_derivative_ne_zero (minpoly.aeval _ _)
+
+end IsLocalRing