From b65f47e3c532ca1c76068a6b1e1f016f90a1b438 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Sat, 28 Feb 2026 17:54:31 -0800
Subject: [PATCH 01/19] feat(RingTheory/IsAdjoinRoot): mkOfAdjoinEqTop'
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Alternative hypothesis to existing theorem: prove the result from a Module.Free hypothesis instead of IsIntegrallyClosed. If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.

Co-authored-by: George Peykanu <gpeyka@uw.edu>
Co-authored-by: Bryan Boehnke <bryanboehnke@gmail.com>
Co-authored-by: Bianca Viray <67076332+b-viray@users.noreply.github.com>
---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 47 ++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index bd15a7128f8f71..40771d448bc5b3 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -622,6 +622,53 @@ theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root =
 
 end mkOfAdjoinEqTop
 
+section mkOfAdjoinEqTop'
+
+variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+
+/-- For finite free modules over a nontrivial ring,
+the degree of the minimal polynomials is bounded by the rank of the module -/
+theorem _root_.minpoly.natDegree_le' (α : S) :
+    (minpoly R α).natDegree ≤ Module.finrank R S := by
+  classical
+  let b := Module.Free.chooseBasis R S
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
+  have haeval : aeval α M.charpoly = 0 := by
+    have h := Matrix.aeval_self_charpoly M
+    rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+      aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
+  exact (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic haeval)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+
+/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
+noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
+    IsAdjoinRootMonic S (minpoly R α) := by
+  set f := minpoly R α
+  have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
+  haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+  let φ : AdjoinRoot f →ₐ[R] S :=
+    AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+  have hφ_surj : Function.Surjective φ := by
+    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+    exact fun s =>
+      let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le' α) (by
+    have e := φ.toLinearMap.quotKerEquivRange.trans
+      (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
+    rw [← e.finrank_eq]
+    exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le)
+  have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
+    ((finrank_quotient_span_eq_natDegree' hf).trans hrank)
+  have hφ_inj : Function.Injective φ :=
+    fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+    (e.symm.toLinearMap.comp φ.toLinearMap) (e.symm.surjective.comp hφ_surj) (congr_arg e.symm h)
+  exact
+    { IsAdjoinRoot.ofAdjoinRootEquiv
+        (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
+
+end mkOfAdjoinEqTop'
+
 section Equiv
 
 variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]

From d601c391f9e60e5bd58eb4ed89b49ed2fb18e5be Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Sat, 28 Feb 2026 19:12:25 -0800
Subject: [PATCH 02/19] feat(LocalRing/Etale): Finite etale extensions are
 monogenic
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Formalization of lemma 3.2 from https://arxiv.org/abs/2503.07846: Given a local finite ring extension R -> S, if the algebraMap is etale, then there exists a β ∈ S such that R[β] = S. Furthermore, if f(z) ∈ R[z] is the minimal polynomial of β, then f′(β) ∈ S×.
---
 Mathlib.lean                            |   1 +
 Mathlib/RingTheory/LocalRing/Etale.lean | 172 ++++++++++++++++++++++++
 2 files changed, 173 insertions(+)
 create mode 100644 Mathlib/RingTheory/LocalRing/Etale.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 9982e285aa34ed..b729663d94d795 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6406,6 +6406,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.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
new file mode 100644
index 00000000000000..11c7df7d7c8615
--- /dev/null
+++ b/Mathlib/RingTheory/LocalRing/Etale.lean
@@ -0,0 +1,172 @@
+/-
+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.Unramified.LocalRing
+public import Mathlib.RingTheory.Smooth.Flat
+public import Mathlib.RingTheory.LocalRing.Module
+public import Mathlib.RingTheory.LocalRing.Quotient
+public import Mathlib.RingTheory.IsAdjoinRoot
+
+/-!
+# É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_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
+  `β 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 in
+/-- 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 (IsLocalRing.ResidueField R)
+    (IsLocalRing.ResidueField S)
+  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
+  refine ⟨β, ?_⟩
+  have h_adjoin_top : Algebra.adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
+    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+      (Algebra.IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
+  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
+    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
+  set mR := IsLocalRing.maximalIdeal R
+  have h_le_sup : (⊤ : Submodule R S) ≤ (Algebra.adjoin R {β}).toSubmodule ⊔ mR • ⊤ := by
+    intro s _
+    obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
+    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
+    rw [Ideal.smul_top_eq_map]
+    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
+    · rw [Algebra.adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
+    · exact (Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
+        Ideal.Quotient.eq.mp
+          (show IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) by
+            rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+              (φ := IsLocalRing.residue R) rfl, hp])
+  exact eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
+    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥) h_le_sup)
+
+-- ResidueField.Basic does not import Algebra stuff.
+/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
+generates `S/m_S` over `R/m_R`. -/
+lemma adjoin_residue_eq_top_of_adjoin_eq_top
+    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
+    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
+  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 (IsLocalRing.residue R),
+    (Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl p β).symm⟩
+
+-- Q: Is this in the right level of generality?
+-- consider adding the maximal ideals mapping as an explicit
+-- hypothesis instead of using Algebra.Etale.
+/-- 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 (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
+  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+  have hmaximal : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) =
+      IsLocalRing.maximalIdeal S := Algebra.FormallyUnramified.map_maximalIdeal
+  let e : (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
+      ≃ₗ[R ⧸ IsLocalRing.maximalIdeal R] (S ⧸ IsLocalRing.maximalIdeal S) :=
+    AddEquiv.toLinearEquiv (Ideal.quotEquivOfEq hmaximal).toAddEquiv (fun r x => by
+      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
+      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
+      simp only [RingEquiv.toAddEquiv_eq_coe]; rfl)
+  erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := S)]
+
+/-- 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 (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
+      (IsLocalRing.residue S β) := by
+  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
+  let kR := IsLocalRing.ResidueField R
+  let β₀ := IsLocalRing.residue S β
+  let f_bar := (minpoly R β).map (IsLocalRing.residue R)
+  have hβ₀_int : IsIntegral kR β₀ := Algebra.IsIntegral.isIntegral β₀
+  -- β₀ is a root of f_bar, so minpoly kR β₀ divides f_bar
+  have hdvd : minpoly kR β₀ ∣ f_bar := minpoly.dvd kR β₀ (by
+    rw [← Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero])
+  have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
+  have hβ₀_field_gen : IntermediateField.adjoin kR {β₀} = ⊤ := by
+    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
+      (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
+    exact IntermediateField.toSubalgebra_injective hβ₀_gen
+  have hdeg_eq : f_bar.natDegree = (minpoly kR β₀).natDegree := by
+    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
+    rw [hmonic.natDegree_map _,
+      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
+      finrank_eq_finrank_residueField, ← IntermediateField.finrank_top', ← hβ₀_field_gen,
+      IntermediateField.adjoin.finrank hβ₀_int]
+  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic hβ₀_int)
+    (hmonic.map _) hdvd hdeg_eq.le
+
+open Polynomial in
+/-- 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 => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
+  let kR := IsLocalRing.ResidueField R
+  let β₀ := IsLocalRing.residue S β
+  have hderiv_ne_zero : aeval β₀ (minpoly kR β₀).derivative ≠ 0 :=
+    (Algebra.IsSeparable.isSeparable kR β₀).aeval_derivative_ne_zero (minpoly.aeval kR β₀)
+  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
+    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
+  exact hderiv_ne_zero
+
+end IsLocalRing
+
+end

From 5a4b0756112cd4a73b6d29a0311213cb4e9698e5 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Wed, 4 Mar 2026 17:07:31 -0800
Subject: [PATCH 03/19] simp lemma + update mathlib

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 40771d448bc5b3..3a6d78634a2358 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -630,23 +630,22 @@ variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 the degree of the minimal polynomials is bounded by the rank of the module -/
 theorem _root_.minpoly.natDegree_le' (α : S) :
     (minpoly R α).natDegree ≤ Module.finrank R S := by
-  classical
-  let b := Module.Free.chooseBasis R S
+  have b := Module.Free.chooseBasis R S
   let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
-  have haeval : aeval α M.charpoly = 0 := by
-    have h := Matrix.aeval_self_charpoly M
-    rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
-      aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
-  exact (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic haeval)).trans
+  refine (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic ?_)).trans
     (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+  let h := Matrix.aeval_self_charpoly M
+  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
 
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
-noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) := by
   set f := minpoly R α
   have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
-  haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+  letI : Module R (AdjoinRoot f) := Algebra.toModule
+  haveI := hf.free_adjoinRoot; haveI finite := hf.finite_adjoinRoot
   let φ : AdjoinRoot f →ₐ[R] S :=
     AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
   have hφ_surj : Function.Surjective φ := by
@@ -667,6 +666,13 @@ noncomputable def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
     { IsAdjoinRoot.ofAdjoinRootEquiv
         (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
 
+@[simp]
+lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
+    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
+    (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
+  unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
+  ext; simp
+
 end mkOfAdjoinEqTop'
 
 section Equiv

From 58230124216425c3171da1b0988fa0946c8ea119 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 16:13:52 -0700
Subject: [PATCH 04/19] move lemmas

---
 Mathlib/FieldTheory/Minpoly/Basic.lean | 16 +++++
 Mathlib/RingTheory/IsAdjoinRoot.lean   | 82 +++++++++++++-------------
 2 files changed, 57 insertions(+), 41 deletions(-)

diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean
index cc1e574160935b..c222fc9f84bbb7 100644
--- a/Mathlib/FieldTheory/Minpoly/Basic.lean
+++ b/Mathlib/FieldTheory/Minpoly/Basic.lean
@@ -6,6 +6,9 @@ Authors: Chris Hughes, Johan Commelin
 module
 
 public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
+public import Mathlib.LinearAlgebra.Dimension.Finrank
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Minimal polynomials
@@ -236,6 +239,19 @@ theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B
   rw [two_le_natDegree_iff int, Iff.not]
   apply Set.ext_iff.mp Subtype.range_val_subtype
 
+omit [Nontrivial B] in
+/-- For finite free modules over a nontrivial ring,
+the degree of the minimal polynomials is bounded by the rank of the module -/
+theorem natDegree_le' [Module.Finite A B] [Module.Free A B] [Nontrivial A] :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
+  let h := Matrix.aeval_self_charpoly M
+  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
+
 end
 
 /-- If `B/A` is an injective ring extension, and `a` is an element of `A`,
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 3a6d78634a2358..fcc4cedca64962 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -622,24 +622,55 @@ theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root =
 
 end mkOfAdjoinEqTop
 
+section Equiv
+
+variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
+
+@[simp]
+theorem lift_algEquiv (i : R →+* U) (x hx z) :
+    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
+
+@[simp]
+theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
+    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
+
+end Equiv
+
+end IsAdjoinRoot
+
+namespace IsAdjoinRootMonic
+
+variable (h : IsAdjoinRootMonic S f)
+
+theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
+  (hirr : Irreducible f) : minpoly R h.root = f :=
+  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
+  symm <|
+    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
+      convert
+        Associated.mul_left (minpoly R h.root) <|
+          associated_one_iff_isUnit.2 <|
+            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
+      rw [mul_one]
+
 section mkOfAdjoinEqTop'
 
 variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 
-/-- For finite free modules over a nontrivial ring,
-the degree of the minimal polynomials is bounded by the rank of the module -/
-theorem _root_.minpoly.natDegree_le' (α : S) :
-    (minpoly R α).natDegree ≤ Module.finrank R S := by
-  have b := Module.Free.chooseBasis R S
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
-  refine (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+-- theorem could be placed here with 0 imports, but
+-- it does not logically make sense.
+theorem alternate_natDegree_le' :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
   let h := Matrix.aeval_self_charpoly M
   rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
     aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
 
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
-def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+def mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) := by
   set f := minpoly R α
@@ -667,7 +698,7 @@ def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
         (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
 
 @[simp]
-lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
+lemma mkOfAdjoinEqTop'_map
     {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
     (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
   unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
@@ -675,37 +706,6 @@ lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
 
 end mkOfAdjoinEqTop'
 
-section Equiv
-
-variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
-
-@[simp]
-theorem lift_algEquiv (i : R →+* U) (x hx z) :
-    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
-
-@[simp]
-theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
-    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
-
-end Equiv
-
-end IsAdjoinRoot
-
-namespace IsAdjoinRootMonic
-
-variable (h : IsAdjoinRootMonic S f)
-
-theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
-  (hirr : Irreducible f) : minpoly R h.root = f :=
-  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
-  symm <|
-    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
-      convert
-        Associated.mul_left (minpoly R h.root) <|
-          associated_one_iff_isUnit.2 <|
-            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
-      rw [mul_one]
-
 end IsAdjoinRootMonic
 
 section Algebra

From 876313ab1ba46aa8dafec7f787e4b4f1199f9bc5 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 16:18:47 -0700
Subject: [PATCH 05/19] Revert "feat(LocalRing/Etale): Finite etale extensions
 are monogenic"

This reverts commit cc73956ac13ce055d398d2cf08f4bf0818a6296c.
---
 Mathlib.lean                            |   1 -
 Mathlib/RingTheory/LocalRing/Etale.lean | 172 ------------------------
 2 files changed, 173 deletions(-)
 delete mode 100644 Mathlib/RingTheory/LocalRing/Etale.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index b729663d94d795..9982e285aa34ed 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6406,7 +6406,6 @@ 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.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
diff --git a/Mathlib/RingTheory/LocalRing/Etale.lean b/Mathlib/RingTheory/LocalRing/Etale.lean
deleted file mode 100644
index 11c7df7d7c8615..00000000000000
--- a/Mathlib/RingTheory/LocalRing/Etale.lean
+++ /dev/null
@@ -1,172 +0,0 @@
-/-
-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.Unramified.LocalRing
-public import Mathlib.RingTheory.Smooth.Flat
-public import Mathlib.RingTheory.LocalRing.Module
-public import Mathlib.RingTheory.LocalRing.Quotient
-public import Mathlib.RingTheory.IsAdjoinRoot
-
-/-!
-# É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_of_adjoin_eq_top`: if `β` generates `S` over `R`, then
-  `β 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 in
-/-- 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 (IsLocalRing.ResidueField R)
-    (IsLocalRing.ResidueField S)
-  obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective β₀
-  refine ⟨β, ?_⟩
-  have h_adjoin_top : Algebra.adjoin (IsLocalRing.ResidueField R) {β₀} = ⊤ := by
-    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-      (Algebra.IsAlgebraic.isAlgebraic β₀), hβ₀, IntermediateField.top_toSubalgebra]
-  rw [show β₀ = IsLocalRing.residue S β from hβ.symm,
-    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at h_adjoin_top
-  set mR := IsLocalRing.maximalIdeal R
-  have h_le_sup : (⊤ : Submodule R S) ≤ (Algebra.adjoin R {β}).toSubmodule ⊔ mR • ⊤ := by
-    intro s _
-    obtain ⟨p, hp⟩ := h_adjoin_top (IsLocalRing.residue S s)
-    obtain ⟨q, rfl⟩ := Polynomial.map_surjective _ IsLocalRing.residue_surjective p
-    rw [Ideal.smul_top_eq_map]
-    refine Submodule.mem_sup.mpr ⟨aeval β q, ?_, s - aeval β q, ?_, by ring⟩
-    · rw [Algebra.adjoin_singleton_eq_range_aeval]; exact ⟨q, rfl⟩
-    · exact (Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)) ▸
-        Ideal.Quotient.eq.mp
-          (show IsLocalRing.residue S s = IsLocalRing.residue S (aeval β q) by
-            rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-              (φ := IsLocalRing.residue R) rfl, hp])
-  exact eq_top_iff.mpr (Submodule.le_of_le_smul_of_le_jacobson_bot
-    (Module.finite_def.mp inferInstance) (IsLocalRing.maximalIdeal_le_jacobson ⊥) h_le_sup)
-
--- ResidueField.Basic does not import Algebra stuff.
-/-- When `β` generates `S` over `R`, the residue `β₀ = β mod m_S`
-generates `S/m_S` over `R/m_R`. -/
-lemma adjoin_residue_eq_top_of_adjoin_eq_top
-    {β : S} (hβ_gen : Algebra.adjoin R {β} = ⊤) :
-    Algebra.adjoin (IsLocalRing.ResidueField R) {IsLocalRing.residue S β} = ⊤ := by
-  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 (IsLocalRing.residue R),
-    (Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl p β).symm⟩
-
--- Q: Is this in the right level of generality?
--- consider adding the maximal ideals mapping as an explicit
--- hypothesis instead of using Algebra.Etale.
-/-- 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 (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) := by
-  haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-  have hmaximal : Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) =
-      IsLocalRing.maximalIdeal S := Algebra.FormallyUnramified.map_maximalIdeal
-  let e : (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
-      ≃ₗ[R ⧸ IsLocalRing.maximalIdeal R] (S ⧸ IsLocalRing.maximalIdeal S) :=
-    AddEquiv.toLinearEquiv (Ideal.quotEquivOfEq hmaximal).toAddEquiv (fun r x => by
-      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
-      obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
-      simp only [RingEquiv.toAddEquiv_eq_coe]; rfl)
-  erw [← e.finrank_eq, IsLocalRing.finrank_quotient_map (R := R) (S := S)]
-
-/-- 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 (IsLocalRing.residue R) = minpoly (IsLocalRing.ResidueField R)
-      (IsLocalRing.residue S β) := by
-  have hmonic := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
-  let kR := IsLocalRing.ResidueField R
-  let β₀ := IsLocalRing.residue S β
-  let f_bar := (minpoly R β).map (IsLocalRing.residue R)
-  have hβ₀_int : IsIntegral kR β₀ := Algebra.IsIntegral.isIntegral β₀
-  -- β₀ is a root of f_bar, so minpoly kR β₀ divides f_bar
-  have hdvd : minpoly kR β₀ ∣ f_bar := minpoly.dvd kR β₀ (by
-    rw [← Polynomial.map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-      (φ := IsLocalRing.residue R) rfl, minpoly.aeval, map_zero])
-  have hβ₀_gen : Algebra.adjoin kR {β₀} = ⊤ := adjoin_residue_eq_top_of_adjoin_eq_top hadj
-  have hβ₀_field_gen : IntermediateField.adjoin kR {β₀} = ⊤ := by
-    rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-      (Algebra.IsAlgebraic.isAlgebraic β₀)] at hβ₀_gen
-    exact IntermediateField.toSubalgebra_injective hβ₀_gen
-  have hdeg_eq : f_bar.natDegree = (minpoly kR β₀).natDegree := by
-    haveI : Module.Free R S := Module.free_of_flat_of_isLocalRing
-    rw [hmonic.natDegree_map _,
-      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
-      finrank_eq_finrank_residueField, ← IntermediateField.finrank_top', ← hβ₀_field_gen,
-      IntermediateField.adjoin.finrank hβ₀_int]
-  exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic hβ₀_int)
-    (hmonic.map _) hdvd hdeg_eq.le
-
-open Polynomial in
-/-- 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 => (IsLocalRing.residue_ne_zero_iff_isUnit s).mp
-  let kR := IsLocalRing.ResidueField R
-  let β₀ := IsLocalRing.residue S β
-  have hderiv_ne_zero : aeval β₀ (minpoly kR β₀).derivative ≠ 0 :=
-    (Algebra.IsSeparable.isSeparable kR β₀).aeval_derivative_ne_zero (minpoly.aeval kR β₀)
-  rw [map_aeval_eq_aeval_map (ψ := IsLocalRing.residue S)
-    (φ := IsLocalRing.residue R) rfl, ← derivative_map, minpoly_map_residue hadj]
-  exact hderiv_ne_zero
-
-end IsLocalRing
-
-end

From e9ccfff2ebb9703d060ba8a61a9ccec3cd8461c6 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 9 Mar 2026 17:23:43 -0700
Subject: [PATCH 06/19] oops fix natDegree_le'

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index fcc4cedca64962..dbac78c190bfa9 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -657,18 +657,6 @@ section mkOfAdjoinEqTop'
 
 variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 
--- theorem could be placed here with 0 imports, but
--- it does not logically make sense.
-theorem alternate_natDegree_le' :
-    (minpoly A x).natDegree ≤ Module.finrank A B := by
-  have b := Module.Free.chooseBasis A B
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
-  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
-  let h := Matrix.aeval_self_charpoly M
-  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
-    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
-
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 def mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
@@ -683,7 +671,7 @@ def mkOfAdjoinEqTop'
     rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
     exact fun s =>
       let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le' α) (by
+  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le') (by
     have e := φ.toLinearMap.quotKerEquivRange.trans
       (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
     rw [← e.finrank_eq]

From 19a085a005d2e61ad69eba2d84390ef680702716 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Tue, 17 Mar 2026 23:32:53 -0700
Subject: [PATCH 07/19] golf away simp lemma

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 64 ++++++++++++----------------
 1 file changed, 27 insertions(+), 37 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index dbac78c190bfa9..fc30f518dd2805 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -653,46 +653,36 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
-section mkOfAdjoinEqTop'
-
-variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
-
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 def mkOfAdjoinEqTop'
+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
-    IsAdjoinRootMonic S (minpoly R α) := by
-  set f := minpoly R α
-  have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
-  letI : Module R (AdjoinRoot f) := Algebra.toModule
-  haveI := hf.free_adjoinRoot; haveI finite := hf.finite_adjoinRoot
-  let φ : AdjoinRoot f →ₐ[R] S :=
-    AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
-  have hφ_surj : Function.Surjective φ := by
-    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
-    exact fun s =>
-      let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le') (by
-    have e := φ.toLinearMap.quotKerEquivRange.trans
-      (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
-    rw [← e.finrank_eq]
-    exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le)
-  have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
-    ((finrank_quotient_span_eq_natDegree' hf).trans hrank)
-  have hφ_inj : Function.Injective φ :=
-    fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-    (e.symm.toLinearMap.comp φ.toLinearMap) (e.symm.surjective.comp hφ_surj) (congr_arg e.symm h)
-  exact
-    { IsAdjoinRoot.ofAdjoinRootEquiv
-        (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
-
-@[simp]
-lemma mkOfAdjoinEqTop'_map
-    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
-    (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
-  unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
-  ext; simp
-
-end mkOfAdjoinEqTop'
+    IsAdjoinRootMonic S (minpoly R α) where
+  map := aeval α
+  ker_map := by
+    set f := minpoly R α
+    have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
+    let φ : AdjoinRoot f →ₐ[R] S :=
+      AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+    have hφ : Function.Surjective φ := by
+      rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+      intro s; obtain ⟨p, hp⟩ := hα s
+      exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+    refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
+    haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+    letI : Module R (AdjoinRoot f) := Algebra.toModule
+    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
+      ((finrank_quotient_span_eq_natDegree' hf).trans <|
+        le_antisymm minpoly.natDegree_le' ?_)
+    · exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+        (e.symm.toLinearMap.comp φ.toLinearMap)
+        (e.symm.surjective.comp hφ) (congr_arg e.symm h)
+    · rw [← φ.toLinearMap.quotKerEquivRange.trans
+        (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ)) |>.finrank_eq]
+      exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le
+  map_surjective := by
+    rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
 end IsAdjoinRootMonic
 

From d50bc8ac1922f0edafa28e976c2b05e8127b33cc Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 6 Apr 2026 16:49:49 -0700
Subject: [PATCH 08/19] use endomorphism cayley-hamilton

---
 Mathlib/FieldTheory/Minpoly/Basic.lean    | 16 ---------------
 Mathlib/LinearAlgebra/Charpoly/Basic.lean | 25 ++++++++++++++++++++---
 Mathlib/RingTheory/IsAdjoinRoot.lean      |  1 +
 3 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean
index c222fc9f84bbb7..cc1e574160935b 100644
--- a/Mathlib/FieldTheory/Minpoly/Basic.lean
+++ b/Mathlib/FieldTheory/Minpoly/Basic.lean
@@ -6,9 +6,6 @@ Authors: Chris Hughes, Johan Commelin
 module
 
 public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
-public import Mathlib.LinearAlgebra.Dimension.Finrank
-import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
-import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Minimal polynomials
@@ -239,19 +236,6 @@ theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B
   rw [two_le_natDegree_iff int, Iff.not]
   apply Set.ext_iff.mp Subtype.range_val_subtype
 
-omit [Nontrivial B] in
-/-- For finite free modules over a nontrivial ring,
-the degree of the minimal polynomials is bounded by the rank of the module -/
-theorem natDegree_le' [Module.Finite A B] [Module.Free A B] [Nontrivial A] :
-    (minpoly A x).natDegree ≤ Module.finrank A B := by
-  have b := Module.Free.chooseBasis A B
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
-  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
-  let h := Matrix.aeval_self_charpoly M
-  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
-    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
-
 end
 
 /-- If `B/A` is an injective ring extension, and `a` is an element of `A`,
diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index d996b467c214c0..6de355d3613342 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -29,9 +29,6 @@ in any basis is in `LinearAlgebra/Charpoly/ToMatrix`.
 
 universe u v w
 
-variable {R : Type u} {M : Type v} [CommRing R]
-variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
-
 open Matrix Polynomial
 
 noncomputable section
@@ -40,6 +37,9 @@ open Module.Free Polynomial Matrix
 
 namespace LinearMap
 
+variable {R : Type u} {M : Type v} [CommRing R]
+variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
+
 section Basic
 
 /-- The characteristic polynomial of `f : M →ₗ[R] M`. -/
@@ -133,3 +133,22 @@ theorem minpoly_coeff_zero_of_injective [Nontrivial R] (hf : Function.Injective
 end CayleyHamilton
 
 end LinearMap
+
+section Algebra
+variable {R M} [CommRing R] [Ring M] [Algebra R M]
+  [Module.Finite R M] [Module.Free R M]
+
+/-- Cayley-Hamilton theorem on general free modules. -/
+theorem Algebra.aeval_self_charpoly_lmul {α : M} :
+    aeval α (Algebra.lmul R M α).charpoly = 0 :=
+  Algebra.lmul_injective (by
+    rw [map_zero, ← aeval_algHom_apply]
+    exact LinearMap.aeval_self_charpoly <| Algebra.lmul R M α)
+
+theorem minpoly.natDegree_le' [Nontrivial R] {α : M} :
+    (minpoly R α).natDegree ≤ Module.finrank R M := by
+  rw [← (Algebra.lmul R M α).charpoly_natDegree]
+  exact natDegree_le_natDegree <|
+    minpoly.min R α (Algebra.lmul R M α).charpoly_monic Algebra.aeval_self_charpoly_lmul
+
+end Algebra
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index fc30f518dd2805..c5539ad068066f 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.RingTheory.PowerBasis
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # A predicate on adjoining roots of polynomial

From 3ddec91d94c09ed42cadd17644c4a1970d772728 Mon Sep 17 00:00:00 2001
From: Grant Yang <38170305+ROTARTSI82@users.noreply.github.com>
Date: Tue, 7 Apr 2026 08:08:05 -0700
Subject: [PATCH 09/19] Apply suggestions from code review

Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>
---
 Mathlib/LinearAlgebra/Charpoly/Basic.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index 6de355d3613342..203d087cab9ef1 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -141,14 +141,12 @@ variable {R M} [CommRing R] [Ring M] [Algebra R M]
 /-- Cayley-Hamilton theorem on general free modules. -/
 theorem Algebra.aeval_self_charpoly_lmul {α : M} :
     aeval α (Algebra.lmul R M α).charpoly = 0 :=
-  Algebra.lmul_injective (by
-    rw [map_zero, ← aeval_algHom_apply]
-    exact LinearMap.aeval_self_charpoly <| Algebra.lmul R M α)
+  Algebra.lmul_injective (R := R) <| by
+    simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
 
 theorem minpoly.natDegree_le' [Nontrivial R] {α : M} :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
-  rw [← (Algebra.lmul R M α).charpoly_natDegree]
-  exact natDegree_le_natDegree <|
-    minpoly.min R α (Algebra.lmul R M α).charpoly_monic Algebra.aeval_self_charpoly_lmul
+simpa [charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
+      (Algebra.lmul R _ α).charpoly_monic Algebra.aeval_self_charpoly
 
 end Algebra

From 00f638afbb1bde556aae25dc6618e02427e2343f Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Tue, 7 Apr 2026 08:14:28 -0700
Subject: [PATCH 10/19] golf + fix simpa

---
 Mathlib/LinearAlgebra/Charpoly/Basic.lean | 5 ++---
 Mathlib/RingTheory/IsAdjoinRoot.lean      | 7 +++----
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index 203d087cab9ef1..c947bd679a92db 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -138,7 +138,6 @@ section Algebra
 variable {R M} [CommRing R] [Ring M] [Algebra R M]
   [Module.Finite R M] [Module.Free R M]
 
-/-- Cayley-Hamilton theorem on general free modules. -/
 theorem Algebra.aeval_self_charpoly_lmul {α : M} :
     aeval α (Algebra.lmul R M α).charpoly = 0 :=
   Algebra.lmul_injective (R := R) <| by
@@ -146,7 +145,7 @@ theorem Algebra.aeval_self_charpoly_lmul {α : M} :
 
 theorem minpoly.natDegree_le' [Nontrivial R] {α : M} :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
-simpa [charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
-      (Algebra.lmul R _ α).charpoly_monic Algebra.aeval_self_charpoly
+  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
+        (Algebra.lmul R _ α).charpoly_monic Algebra.aeval_self_charpoly_lmul
 
 end Algebra
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index b4ac21022ed763..0655d5b7f99f24 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -666,15 +666,14 @@ def mkOfAdjoinEqTop'
     refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
     haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
     letI : Module R (AdjoinRoot f) := Algebra.toModule
-    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
-      ((finrank_quotient_span_eq_natDegree' hf).trans <|
-        le_antisymm minpoly.natDegree_le' ?_)
+    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le') ?_
     · exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
         (e.symm.toLinearMap.comp φ.toLinearMap)
         (e.symm.surjective.comp hφ) (congr_arg e.symm h)
     · rw [← φ.toLinearMap.quotKerEquivRange.trans
         (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ)) |>.finrank_eq]
-      exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le
+      exact Submodule.finrank_quotient_le _
   map_surjective := by
     rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)

From b02c2f8ed6551630e41fd6bac1fa7905698697e8 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Tue, 7 Apr 2026 11:59:05 -0700
Subject: [PATCH 11/19] LinearMap.finrank_le_finrank_of_surjective

---
 Mathlib/LinearAlgebra/Dimension/Constructions.lean |  6 ++++++
 Mathlib/RingTheory/IsAdjoinRoot.lean               | 12 +++++-------
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
index 095a6462a8ff75..a68aacaca1cbf5 100644
--- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
@@ -104,6 +104,12 @@ theorem Submodule.finrank_quotient_le [StrongRankCondition R] [Module.Finite R M
   toNat_le_toNat ((Submodule.mkQ s).rank_le_of_surjective Quot.mk_surjective)
     (rank_lt_aleph0 _ _)
 
+theorem LinearMap.finrank_le_finrank_of_surjective
+    [Module R M'] [StrongRankCondition R] [Module.Finite R M]
+    {f : M →ₗ[R] M'} (h : Function.Surjective f) : Module.finrank R M' ≤ Module.finrank R M := by
+  rw [← f.quotKerEquivOfSurjective h |>.finrank_eq]
+  exact Submodule.finrank_quotient_le _
+
 end Quotient
 
 variable [Semiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M₁]
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 0655d5b7f99f24..70b5c97516cfa6 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -667,13 +667,11 @@ def mkOfAdjoinEqTop'
     haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
     letI : Module R (AdjoinRoot f) := Algebra.toModule
     have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
-        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le') ?_
-    · exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-        (e.symm.toLinearMap.comp φ.toLinearMap)
-        (e.symm.surjective.comp hφ) (congr_arg e.symm h)
-    · rw [← φ.toLinearMap.quotKerEquivRange.trans
-        (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ)) |>.finrank_eq]
-      exact Submodule.finrank_quotient_le _
+      le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le')
+      (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
+    exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+      (e.symm.toLinearMap.comp φ.toLinearMap)
+      (e.symm.surjective.comp hφ) (congr_arg e.symm h)
   map_surjective := by
     rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)

From 2314a3d4ae3c721d1dbd2f0a228e3d2a5c70d27c Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Thu, 9 Apr 2026 13:04:09 -0700
Subject: [PATCH 12/19] OrzechProperty.bijective_of_surjective_of_finrank_le

Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>
---
 Mathlib/LinearAlgebra/Charpoly/Basic.lean     |  6 ++--
 .../Dimension/Constructions.lean              | 36 +++++++++++++++++++
 Mathlib/RingTheory/IsAdjoinRoot.lean          | 36 +++++++++----------
 Mathlib/RingTheory/OrzechProperty.lean        |  6 ++++
 4 files changed, 63 insertions(+), 21 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index c947bd679a92db..1e7e974368bb3a 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -138,14 +138,14 @@ section Algebra
 variable {R M} [CommRing R] [Ring M] [Algebra R M]
   [Module.Finite R M] [Module.Free R M]
 
-theorem Algebra.aeval_self_charpoly_lmul {α : M} :
+theorem Algebra.aeval_self_charpoly_lmul (α : M) :
     aeval α (Algebra.lmul R M α).charpoly = 0 :=
   Algebra.lmul_injective (R := R) <| by
     simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
 
-theorem minpoly.natDegree_le' [Nontrivial R] {α : M} :
+theorem minpoly.natDegree_le' [Nontrivial R] (α : M) :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
   simpa [← (Algebra.lmul _ _ α).charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
-        (Algebra.lmul R _ α).charpoly_monic Algebra.aeval_self_charpoly_lmul
+    (Algebra.lmul R _ α).charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
 
 end Algebra
diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
index a68aacaca1cbf5..76429d609ccad1 100644
--- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
@@ -335,6 +335,42 @@ theorem Module.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by sim
 
 variable {R}
 
+theorem Module.le_rank_iff_exists_linearMap'
+    [Module R M'] [Module.Finite R M] [Nontrivial R] :
+    Module.finrank R M ≤ Module.rank R M' ↔
+      ∃ f : M →ₗ[R] M', Function.Injective f :=
+  let e := LinearEquiv.ofFinrankEq (R := R) M
+    (Fin (Module.finrank R M) → R) (Module.finrank_fin_fun R).symm
+  ⟨
+    fun h => by
+      rw [Module.le_rank_iff_exists_linearMap] at h
+      rcases h with ⟨φ, hφ⟩
+      exact ⟨φ ∘ₛₗ e.toLinearMap, by simpa⟩,
+    fun ⟨f, hf⟩ => Module.le_rank_iff_exists_linearMap.mpr
+      ⟨f ∘ₛₗ e.symm.toLinearMap, by simpa⟩
+  ⟩
+
+theorem Module.le_finrank_iff_existsLinearMap
+    [Module R M'] [Module.Finite R M] [Nontrivial R] [Module.Finite R M'] :
+    Module.finrank R M ≤ Module.finrank R M' ↔
+      ∃ f : M →ₗ[R] M', Function.Injective f :=
+  ⟨
+    fun h => Module.le_rank_iff_exists_linearMap'.mp <| by
+      rw [← Module.finrank_eq_rank R M', Nat.cast_le]
+      exact h,
+    fun h => by
+      let h := Module.le_rank_iff_exists_linearMap'.mpr h
+      rwa [← Module.finrank_eq_rank R M', Nat.cast_le] at h
+  ⟩
+
+theorem OrzechProperty.bijective_of_surjective_of_finrank_le [OrzechProperty R]
+    [Module R M'] [Module.Finite R M] [Nontrivial R] [Module.Finite R M']
+    (h : Module.finrank R M ≤ Module.finrank R M')
+    (f : M →ₗ[R] M') (hf : Function.Surjective f) :
+    Function.Bijective f := by
+  rcases Module.le_finrank_iff_existsLinearMap.mp h with ⟨φ, hφ⟩
+  refine OrzechProperty.bijective_of_surjective_of_injective φ _ hφ hf
+
 -- TODO: merge with the `Finrank` content
 /-- An `n`-dimensional `R`-vector space is equivalent to `Fin n → R`. -/
 def finDimVectorspaceEquiv (n : ℕ) (hn : Module.rank R M = n) : M ≃ₗ[R] Fin n → R := by
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 70b5c97516cfa6..702b4d03df7c28 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -653,27 +653,27 @@ def mkOfAdjoinEqTop'
     [Module.Finite R S] [Module.Free R S] [Nontrivial R]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) where
-  map := aeval α
-  ker_map := by
-    set f := minpoly R α
+  __ : IsAdjoinRoot S (minpoly R α) :=
+    let f := minpoly R α
     have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
     let φ : AdjoinRoot f →ₐ[R] S :=
       AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
-    have hφ : Function.Surjective φ := by
-      rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
-      intro s; obtain ⟨p, hp⟩ := hα s
-      exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-    refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
-    haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
-    letI : Module R (AdjoinRoot f) := Algebra.toModule
-    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
-      le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le')
-      (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
-    exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-      (e.symm.toLinearMap.comp φ.toLinearMap)
-      (e.symm.surjective.comp hφ) (congr_arg e.symm h)
-  map_surjective := by
-    rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+    IsAdjoinRoot.ofAdjoinRootEquiv <| AlgEquiv.ofBijective φ <| by
+      have hφ : Function.Surjective φ := by
+        rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+        intro s; obtain ⟨p, hp⟩ := hα s
+        exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+      haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+      letI : Module R (AdjoinRoot f) := Algebra.toModule
+      -- exact OrzechProperty.bijective_of_surjective_of_finrank_le
+      --  (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α) φ hφ
+      have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α)
+        (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
+      exact ⟨fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+        (e.symm.toLinearMap.comp φ.toLinearMap)
+        (e.symm.surjective.comp hφ) (congr_arg e.symm h), hφ⟩
+  map := aeval α
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
 end IsAdjoinRootMonic
diff --git a/Mathlib/RingTheory/OrzechProperty.lean b/Mathlib/RingTheory/OrzechProperty.lean
index 00a29d6aefd18d..584b792970015d 100644
--- a/Mathlib/RingTheory/OrzechProperty.lean
+++ b/Mathlib/RingTheory/OrzechProperty.lean
@@ -91,6 +91,12 @@ theorem injective_of_surjective_of_injective
   replace hf : Surjective f' := by simpa [f'] using hf
   simpa [f'] using injective_of_surjective_of_submodule' f' hf
 
+theorem bijective_of_surjective_of_injective
+    {N : Type w} [AddCommMonoid N] [Module R N]
+    (i f : N →ₗ[R] M) (hi : Function.Injective i)
+    (hf : Function.Surjective f) : Function.Bijective f :=
+  ⟨OrzechProperty.injective_of_surjective_of_injective _ _ hi hf, hf⟩
+
 theorem injective_of_surjective_of_submodule
     {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
   injective_of_surjective_of_injective N.subtype f N.injective_subtype hf

From 821cdc514ab529c1f7824500c8011e5122711342 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Thu, 9 Apr 2026 13:11:52 -0700
Subject: [PATCH 13/19] invoke in mkOfAdjoinEqTop'

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 702b4d03df7c28..84e5f6ec272364 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -665,14 +665,8 @@ def mkOfAdjoinEqTop'
         exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
       haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
       letI : Module R (AdjoinRoot f) := Algebra.toModule
-      -- exact OrzechProperty.bijective_of_surjective_of_finrank_le
-      --  (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α) φ hφ
-      have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
-        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α)
-        (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
-      exact ⟨fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-        (e.symm.toLinearMap.comp φ.toLinearMap)
-        (e.symm.surjective.comp hφ) (congr_arg e.symm h), hφ⟩
+      exact OrzechProperty.bijective_of_surjective_of_finrank_le
+       (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α) φ.toLinearMap hφ
   map := aeval α
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 

From 11552b232167cae812447bb67a73a5199871da21 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Fri, 10 Apr 2026 17:25:20 -0700
Subject: [PATCH 14/19] unprime minpoly.natDegree_le

---
 Mathlib/Analysis/Complex/Polynomial/Basic.lean           | 8 ++++----
 Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean  | 9 ---------
 Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean              | 1 +
 Mathlib/FieldTheory/Normal/Basic.lean                    | 1 +
 Mathlib/FieldTheory/PurelyInseparable/Exponent.lean      | 1 +
 Mathlib/LinearAlgebra/Charpoly/Basic.lean                | 6 +++++-
 .../NumberField/InfinitePlace/Embeddings.lean            | 1 +
 Mathlib/RingTheory/IsAdjoinRoot.lean                     | 7 +++++++
 8 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Analysis/Complex/Polynomial/Basic.lean b/Mathlib/Analysis/Complex/Polynomial/Basic.lean
index f3c0eb31214358..1e56b615ceee42 100644
--- a/Mathlib/Analysis/Complex/Polynomial/Basic.lean
+++ b/Mathlib/Analysis/Complex/Polynomial/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Complex.Liouville
 public import Mathlib.FieldTheory.PolynomialGaloisGroup
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.Topology.Algebra.Polynomial
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # The fundamental theorem of algebra
@@ -198,10 +199,9 @@ lemma Irreducible.natDegree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree
   obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
     IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
   rw [← finrank_real_complex]
-  convert minpoly.natDegree_le z using 1
-  · rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
-      natDegree_C, add_zero]
-  infer_instance
+  suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (R := ℝ) z
+  rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
+    natDegree_C, add_zero]
 
 /-- An irreducible real polynomial has degree at most two. -/
 lemma Irreducible.degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤ 2 :=
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
index bd0f3430685ce6..d9e729b245b01a 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -531,15 +531,6 @@ theorem exists_lt_finrank_of_infinite_dimensional
     have h2 : F⟮x⟯ ≤ L' := le_sup_right
     exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
 
-theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] :
-    (minpoly K x).natDegree ≤ finrank K L :=
-  le_of_eq_of_le (IntermediateField.adjoin.finrank (.of_finite _ _)).symm
-    K⟮x⟯.toSubmodule.finrank_le
-
-theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] :
-    (minpoly K x).degree ≤ finrank K L :=
-  degree_le_of_natDegree_le (minpoly.natDegree_le x)
-
 /-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the
   minimal polynomial of `x` over `K` divides `[L : K]`. -/
 theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) :
diff --git a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
index f508b6741c04d5..2a91163c71d537 100644
--- a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
+++ b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.FieldTheory.PrimitiveElement
 public import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Results about `minpoly R x / (X - C x)`
diff --git a/Mathlib/FieldTheory/Normal/Basic.lean b/Mathlib/FieldTheory/Normal/Basic.lean
index 4bd92293c88905..c11882fec95c20 100644
--- a/Mathlib/FieldTheory/Normal/Basic.lean
+++ b/Mathlib/FieldTheory/Normal/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.FieldTheory.Extension
 public import Mathlib.FieldTheory.Normal.Defs
 public import Mathlib.GroupTheory.Solvable
 public import Mathlib.FieldTheory.SplittingField.Construction
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Normal field extensions
diff --git a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
index 5c64e8389b25d8..ff27e5fcf40f30 100644
--- a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
+++ b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
@@ -6,6 +6,7 @@ Authors: Michal Staromiejski
 module
 
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 
diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index 1e7e974368bb3a..b6416ee56bb981 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -143,9 +143,13 @@ theorem Algebra.aeval_self_charpoly_lmul (α : M) :
   Algebra.lmul_injective (R := R) <| by
     simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
 
-theorem minpoly.natDegree_le' [Nontrivial R] (α : M) :
+theorem minpoly.natDegree_le [Nontrivial R] (α : M) :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
   simpa [← (Algebra.lmul _ _ α).charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
     (Algebra.lmul R _ α).charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
 
+theorem minpoly.degree_le [Nontrivial R] (α : M) :
+    (minpoly R α).degree ≤ Module.finrank R M :=
+  degree_le_of_natDegree_le (minpoly.natDegree_le α)
+
 end Algebra
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
index ea6a83b45f797e..99b1296830cc63 100644
--- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Hom.Rat
 public import Mathlib.Analysis.Complex.Polynomial.Basic
 public import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Embeddings of number fields
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 84e5f6ec272364..4c81362f4f3a50 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -670,6 +670,13 @@ def mkOfAdjoinEqTop'
   map := aeval α
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
+@[simp]
+theorem mkOfAdjoinEqTop'_root
+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
+      (mkOfAdjoinEqTop' hα).root = α := by
+  simp [mkOfAdjoinEqTop', IsAdjoinRoot.root]
+
 end IsAdjoinRootMonic
 
 section Algebra

From 9ed017f2dd3f752a434a3b682164806602c606d4 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Fri, 10 Apr 2026 18:00:58 -0700
Subject: [PATCH 15/19] revert
 OrzechProperty.bijective_of_surjective_of_finrank_le + fixes

The theorems in Constructions.lean are generalized by
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Embedding.20free.20modules.20into.20each.20other/near/584518236
and so we will wait for that PR.

Actually, maybe the iff is valuable? idk.
---
 .../Dimension/Constructions.lean              | 36 -------------------
 Mathlib/RingTheory/IsAdjoinRoot.lean          |  7 ++--
 Mathlib/RingTheory/Valuation/Minpoly.lean     |  1 +
 3 files changed, 6 insertions(+), 38 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
index 76429d609ccad1..a68aacaca1cbf5 100644
--- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
@@ -335,42 +335,6 @@ theorem Module.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by sim
 
 variable {R}
 
-theorem Module.le_rank_iff_exists_linearMap'
-    [Module R M'] [Module.Finite R M] [Nontrivial R] :
-    Module.finrank R M ≤ Module.rank R M' ↔
-      ∃ f : M →ₗ[R] M', Function.Injective f :=
-  let e := LinearEquiv.ofFinrankEq (R := R) M
-    (Fin (Module.finrank R M) → R) (Module.finrank_fin_fun R).symm
-  ⟨
-    fun h => by
-      rw [Module.le_rank_iff_exists_linearMap] at h
-      rcases h with ⟨φ, hφ⟩
-      exact ⟨φ ∘ₛₗ e.toLinearMap, by simpa⟩,
-    fun ⟨f, hf⟩ => Module.le_rank_iff_exists_linearMap.mpr
-      ⟨f ∘ₛₗ e.symm.toLinearMap, by simpa⟩
-  ⟩
-
-theorem Module.le_finrank_iff_existsLinearMap
-    [Module R M'] [Module.Finite R M] [Nontrivial R] [Module.Finite R M'] :
-    Module.finrank R M ≤ Module.finrank R M' ↔
-      ∃ f : M →ₗ[R] M', Function.Injective f :=
-  ⟨
-    fun h => Module.le_rank_iff_exists_linearMap'.mp <| by
-      rw [← Module.finrank_eq_rank R M', Nat.cast_le]
-      exact h,
-    fun h => by
-      let h := Module.le_rank_iff_exists_linearMap'.mpr h
-      rwa [← Module.finrank_eq_rank R M', Nat.cast_le] at h
-  ⟩
-
-theorem OrzechProperty.bijective_of_surjective_of_finrank_le [OrzechProperty R]
-    [Module R M'] [Module.Finite R M] [Nontrivial R] [Module.Finite R M']
-    (h : Module.finrank R M ≤ Module.finrank R M')
-    (f : M →ₗ[R] M') (hf : Function.Surjective f) :
-    Function.Bijective f := by
-  rcases Module.le_finrank_iff_existsLinearMap.mp h with ⟨φ, hφ⟩
-  refine OrzechProperty.bijective_of_surjective_of_injective φ _ hφ hf
-
 -- TODO: merge with the `Finrank` content
 /-- An `n`-dimensional `R`-vector space is equivalent to `Fin n → R`. -/
 def finDimVectorspaceEquiv (n : ℕ) (hn : Module.rank R M = n) : M ≃ₗ[R] Fin n → R := by
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 4c81362f4f3a50..9e3af8a522b6bc 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -665,8 +665,11 @@ def mkOfAdjoinEqTop'
         exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
       haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
       letI : Module R (AdjoinRoot f) := Algebra.toModule
-      exact OrzechProperty.bijective_of_surjective_of_finrank_le
-       (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le' α) φ.toLinearMap hφ
+      have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
+        (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
+      exact OrzechProperty.bijective_of_surjective_of_injective
+        e.toLinearMap φ e.injective hφ
   map := aeval α
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
diff --git a/Mathlib/RingTheory/Valuation/Minpoly.lean b/Mathlib/RingTheory/Valuation/Minpoly.lean
index 2326e90b1063dd..031fd098d1ecc6 100644
--- a/Mathlib/RingTheory/Valuation/Minpoly.lean
+++ b/Mathlib/RingTheory/Valuation/Minpoly.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
 public import Mathlib.RingTheory.Valuation.Basic
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Minimal polynomials.

From db4fd801c4d8de036a602bfe3c170fada5177f68 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 13 Apr 2026 12:57:22 -0700
Subject: [PATCH 16/19] rm Nontrivial + public import + golf

Co-authored-by: <riccardo.brasca@gmail.com>
---
 Mathlib/Analysis/Complex/Polynomial/Basic.lean |  2 +-
 Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean    |  2 +-
 Mathlib/FieldTheory/Normal/Basic.lean          |  2 +-
 Mathlib/LinearAlgebra/Charpoly/Basic.lean      | 18 ++++++++++++------
 .../NumberField/InfinitePlace/Embeddings.lean  |  2 +-
 Mathlib/RingTheory/IsAdjoinRoot.lean           | 10 ++++++----
 Mathlib/RingTheory/Valuation/Minpoly.lean      |  2 +-
 7 files changed, 23 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Analysis/Complex/Polynomial/Basic.lean b/Mathlib/Analysis/Complex/Polynomial/Basic.lean
index 1e56b615ceee42..7a6730863a1c8c 100644
--- a/Mathlib/Analysis/Complex/Polynomial/Basic.lean
+++ b/Mathlib/Analysis/Complex/Polynomial/Basic.lean
@@ -10,7 +10,7 @@ public import Mathlib.Analysis.Complex.Liouville
 public import Mathlib.FieldTheory.PolynomialGaloisGroup
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.Topology.Algebra.Polynomial
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # The fundamental theorem of algebra
diff --git a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
index 2a91163c71d537..57d99d951dc80f 100644
--- a/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
+++ b/Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.FieldTheory.PrimitiveElement
 public import Mathlib.FieldTheory.IsAlgClosed.Basic
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Results about `minpoly R x / (X - C x)`
diff --git a/Mathlib/FieldTheory/Normal/Basic.lean b/Mathlib/FieldTheory/Normal/Basic.lean
index c11882fec95c20..6f5196a9efd2c4 100644
--- a/Mathlib/FieldTheory/Normal/Basic.lean
+++ b/Mathlib/FieldTheory/Normal/Basic.lean
@@ -9,7 +9,7 @@ public import Mathlib.FieldTheory.Extension
 public import Mathlib.FieldTheory.Normal.Defs
 public import Mathlib.GroupTheory.Solvable
 public import Mathlib.FieldTheory.SplittingField.Construction
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Normal field extensions
diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index b6416ee56bb981..0fc357bacdba78 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -75,8 +75,9 @@ theorem charpoly_monic : f.charpoly.Monic :=
   Matrix.charpoly_monic _
 
 open Module in
-lemma charpoly_natDegree [Nontrivial R] [StrongRankCondition R] :
+lemma charpoly_natDegree [StrongRankCondition R] :
     natDegree (charpoly f) = finrank R M := by
+  haveI := nontrivial_of_invariantBasisNumber
   rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
 
 end Coeff
@@ -143,12 +144,17 @@ theorem Algebra.aeval_self_charpoly_lmul (α : M) :
   Algebra.lmul_injective (R := R) <| by
     simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
 
-theorem minpoly.natDegree_le [Nontrivial R] (α : M) :
+theorem minpoly.natDegree_le (α : M) :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
-  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
-    (Algebra.lmul R _ α).charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
-
-theorem minpoly.degree_le [Nontrivial R] (α : M) :
+  by_cases h : Nontrivial R
+  · let f := Algebra.lmul R _ α
+    have : (minpoly R α).natDegree ≤ f.charpoly.natDegree := natDegree_le_natDegree <|
+      minpoly.min _ _ f.charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
+    simpa [← (Algebra.lmul _ _ α).charpoly_natDegree]
+  · haveI := not_nontrivial_iff_subsingleton.mp h
+    simp [natDegree_of_subsingleton]
+
+theorem minpoly.degree_le (α : M) :
     (minpoly R α).degree ≤ Module.finrank R M :=
   degree_le_of_natDegree_le (minpoly.natDegree_le α)
 
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
index 99b1296830cc63..3d4f81aecdd937 100644
--- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
+++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Hom.Rat
 public import Mathlib.Analysis.Complex.Polynomial.Basic
 public import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Embeddings of number fields
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 9e3af8a522b6bc..f1b0244da8eb51 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.RingTheory.PowerBasis
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # A predicate on adjoining roots of polynomial
@@ -648,7 +648,10 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
-/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
+/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.
+
+Takes the hypothesis that `S` is a free and finitely generated R-module,
+unlike `mkOfAdjoinEqTop` which takes that `R` is an integral domain. -/
 def mkOfAdjoinEqTop'
     [Module.Finite R S] [Module.Free R S] [Nontrivial R]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
@@ -664,8 +667,7 @@ def mkOfAdjoinEqTop'
         intro s; obtain ⟨p, hp⟩ := hα s
         exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
       haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
-      letI : Module R (AdjoinRoot f) := Algebra.toModule
-      have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+      letI e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
         le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
         (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
       exact OrzechProperty.bijective_of_surjective_of_injective
diff --git a/Mathlib/RingTheory/Valuation/Minpoly.lean b/Mathlib/RingTheory/Valuation/Minpoly.lean
index 031fd098d1ecc6..59d6160f1dd987 100644
--- a/Mathlib/RingTheory/Valuation/Minpoly.lean
+++ b/Mathlib/RingTheory/Valuation/Minpoly.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
 public import Mathlib.RingTheory.Valuation.Basic
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Minimal polynomials.

From fedc305a28aaca0ec936392ea226fb257d943ca3 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Mon, 13 Apr 2026 13:01:15 -0700
Subject: [PATCH 17/19] missed public import

---
 Mathlib/FieldTheory/PurelyInseparable/Exponent.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
index ff27e5fcf40f30..c1392acce96683 100644
--- a/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
+++ b/Mathlib/FieldTheory/PurelyInseparable/Exponent.lean
@@ -6,7 +6,7 @@ Authors: Michal Staromiejski
 module
 
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
-import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 

From c2b0980d56eb8cbb0e3f22c0ff5db80974c51a0e Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Tue, 14 Apr 2026 10:05:38 -0700
Subject: [PATCH 18/19] rm another Nontrivial + simp API + golf

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
---
 Mathlib/LinearAlgebra/Charpoly/Basic.lean | 12 ++++-----
 Mathlib/RingTheory/IsAdjoinRoot.lean      | 30 +++++++++++++----------
 2 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
index 0fc357bacdba78..90c9b25393ec1a 100644
--- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean
+++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean
@@ -146,13 +146,11 @@ theorem Algebra.aeval_self_charpoly_lmul (α : M) :
 
 theorem minpoly.natDegree_le (α : M) :
     (minpoly R α).natDegree ≤ Module.finrank R M := by
-  by_cases h : Nontrivial R
-  · let f := Algebra.lmul R _ α
-    have : (minpoly R α).natDegree ≤ f.charpoly.natDegree := natDegree_le_natDegree <|
-      minpoly.min _ _ f.charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
-    simpa [← (Algebra.lmul _ _ α).charpoly_natDegree]
-  · haveI := not_nontrivial_iff_subsingleton.mp h
-    simp [natDegree_of_subsingleton]
+  nontriviality R
+  let f := Algebra.lmul R _ α
+  have : (minpoly R α).natDegree ≤ f.charpoly.natDegree := natDegree_le_natDegree <|
+    minpoly.min _ _ f.charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
+  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree]
 
 theorem minpoly.degree_le (α : M) :
     (minpoly R α).degree ≤ Module.finrank R M :=
diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index f1b0244da8eb51..9462de2b3927fa 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -648,12 +648,12 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
-/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.
-
-Takes the hypothesis that `S` is a free and finitely generated R-module,
-unlike `mkOfAdjoinEqTop` which takes that `R` is an integral domain. -/
+/-- If `α` generates `S` as an algebra and `S` is free and finite,
+then `S` is given by adjoining a root of `minpoly R α`.
+Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop` -/
+@[simps]
 def mkOfAdjoinEqTop'
-    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+    [Module.Finite R S] [Module.Free R S]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) where
   __ : IsAdjoinRoot S (minpoly R α) :=
@@ -667,20 +667,24 @@ def mkOfAdjoinEqTop'
         intro s; obtain ⟨p, hp⟩ := hα s
         exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
       haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
-      letI e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
-        le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
-        (LinearMap.finrank_le_finrank_of_surjective (f:=φ.toLinearMap) hφ)
-      exact OrzechProperty.bijective_of_surjective_of_injective
-        e.toLinearMap φ e.injective hφ
+      by_cases h : Nontrivial R
+      · letI e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+          le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
+          (LinearMap.finrank_le_finrank_of_surjective (f := φ.toLinearMap) hφ)
+        exact OrzechProperty.bijective_of_surjective_of_injective
+          e.toLinearMap φ e.injective hφ
+      · apply not_nontrivial_iff_subsingleton.mp at h
+        haveI := Module.subsingleton R (AdjoinRoot f)
+        exact ⟨Function.injective_of_subsingleton φ, hφ⟩
   map := aeval α
   monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
 @[simp]
 theorem mkOfAdjoinEqTop'_root
-    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
-    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
+    [Module.Finite R S] [Module.Free R S]
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
       (mkOfAdjoinEqTop' hα).root = α := by
-  simp [mkOfAdjoinEqTop', IsAdjoinRoot.root]
+  simp [IsAdjoinRoot.root]
 
 end IsAdjoinRootMonic
 

From 75af86c9b30828c3ebfbc733544a90fe6076c552 Mon Sep 17 00:00:00 2001
From: Grant Yang <rotartsi0482@gmail.com>
Date: Wed, 15 Apr 2026 11:32:44 -0700
Subject: [PATCH 19/19] simp lemmas for mkOfAdjoinEqTop (unprimed)

---
 Mathlib/RingTheory/IsAdjoinRoot.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean
index 9462de2b3927fa..f124a99711a054 100644
--- a/Mathlib/RingTheory/IsAdjoinRoot.lean
+++ b/Mathlib/RingTheory/IsAdjoinRoot.lean
@@ -592,10 +592,10 @@ end lift
 section mkOfAdjoinEqTop
 
 variable [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
-    {α : S} {hα : IsIntegral R α} {hα₂ : Algebra.adjoin R {α} = ⊤}
+    {α : S} (hα : IsIntegral R α) (hα₂ : Algebra.adjoin R {α} = ⊤)
 
-variable (hα hα₂) in
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
+@[simps]
 def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
   map := aeval α
   map_surjective := by
@@ -605,7 +605,6 @@ def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
     ext
     simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _
 
-variable (hα hα₂) in
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R α) where
   __ := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
@@ -613,7 +612,7 @@ abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R
 
 @[simp]
 theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α := by
-  simp [IsAdjoinRoot.mkOfAdjoinEqTop, IsAdjoinRoot.root]
+  simp [IsAdjoinRoot.root]
 
 end mkOfAdjoinEqTop
 
@@ -650,7 +649,7 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
 
 /-- If `α` generates `S` as an algebra and `S` is free and finite,
 then `S` is given by adjoining a root of `minpoly R α`.
-Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop` -/
+Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop`. -/
 @[simps]
 def mkOfAdjoinEqTop'
     [Module.Finite R S] [Module.Free R S]