[Merged by Bors] - feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' by ROTARTSI82 · Pull Request #36421 · leanprover-community/mathlib4

ROTARTSI82 · 2026-03-10T00:38:19Z

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 α.

Hello, we are the Algebraic Geometry group from the UW Math AI lab, and this is our first PR! This definition of mkOfAdjoinEqTop' generalizes the existing mkOfAdjoinEqTop and shows the result from Module.Free instead of IsIntegrallyClosed. It is used in future results that we would like to upstream at https://github.com/uw-math-ai/monogenic-extensions, which is a project to formalize lemmas 3.1 and 3.2 from https://arxiv.org/abs/2503.07846.

AI Usage: Claude code and Aristotle were used to fill sorries and search mathlib for existing lemmas, and the code was then golfed by hand.

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

-->

github-actions · 2026-03-10T00:38:28Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-03-10T00:39:33Z

PR summary 00dbc4ec64

Import changes exceeding 2%

%	File
+2.31%	`Mathlib.FieldTheory.Normal.Basic`
+3.23%	`Mathlib.RingTheory.IsAdjoinRoot`
+2.37%	`Mathlib.RingTheory.Valuation.Minpoly`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.IsAdjoinRoot	1671	1725	+54 (+3.23%)
Mathlib.RingTheory.Valuation.Minpoly	1686	1726	+40 (+2.37%)
Mathlib.FieldTheory.Normal.Basic	1686	1725	+39 (+2.31%)
Mathlib.FieldTheory.Minpoly.MinpolyDiv	1747	1748	+1 (+0.06%)
Mathlib.FieldTheory.PurelyInseparable.Exponent	1780	1781	+1 (+0.06%)
Mathlib.Analysis.Complex.Polynomial.Basic	2624	2625	+1 (+0.04%)
Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings	2696	2697	+1 (+0.04%)

Import changes for all files

Files	Import difference
224 files `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.Fuglede` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.Projection` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitary.Connected` `Mathlib.Analysis.CStarAlgebra.Unitary.Span` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.GaussLucas` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Measure` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.InnerProductSpace.StandardSubspace` `Mathlib.Analysis.Normed.Algebra.GelfandFormula` `Mathlib.Analysis.Normed.Algebra.GelfandMazur` `Mathlib.Analysis.Normed.Field.Dense` `Mathlib.Analysis.Normed.Field.Krasner` `Mathlib.Analysis.Normed.Unbundled.SpectralNorm` `Mathlib.Analysis.Polynomial.Factorization` `Mathlib.Analysis.Polynomial.MahlerMeasure` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Finite.Extension` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.SeparablyGenerated` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.InfinitePlace` `Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormalClosure` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Field` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Dedekind` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Valued.WithVal`	1
`Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure`	39
`Mathlib.RingTheory.Valuation.Minpoly`	40
`Mathlib.NumberTheory.KummerDedekind`	50
`Mathlib.RingTheory.IsAdjoinRoot`	54

Declarations diff

+ Algebra.aeval_self_charpoly_lmul
+ LinearMap.finrank_le_finrank_of_surjective
+ bijective_of_surjective_of_injective
+ minpoly.degree_le
+ minpoly.natDegree_le
+ mkOfAdjoinEqTop'
+ mkOfAdjoinEqTop'_root
- _root_.minpoly.degree_le
- _root_.minpoly.natDegree_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

ROTARTSI82 · 2026-03-12T02:41:11Z

t-algebra

For the large import changes, we are a bit unsure about the placement of the minpoly.natDegree_le' lemma into Minpoly.Basic, and feedback would very much be appreciated! That lemma could be placed into IsAdjoinRoot.lean with no new imports, but organizationally that does not make sense.

Zulip thread?

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>

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×.

This reverts commit cc73956.

b-viray · 2026-03-21T18:34:25Z

t-ring-theory

artie2000 · 2026-04-05T20:06:10Z

One question: I see a CLAUDE.md in your downstream repo. Please disclose whether and how AI was used to create this PR per our policy.

This particular PR is clearly of value - but knowing this information helps reviewers like me know what sorts of problems to look out for, because humans and AI diverge from Mathlib contribution guidelines differently.

artie2000

In Mathlib we aim to prove everything in the maximal possible sensible generality. Your proofs can be broken up into much smaller lemmas, adding missing API as necessary. Please double check the maths because I'm not an expert, but I think it all works out.

This tool is good for finding lemmas: https://leandex.projectnumina.ai/

artie2000 · 2026-04-05T21:19:28Z

awaiting-author

Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>

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.

artie2000 · 2026-04-11T02:02:21Z

Sibling PRs: #37872, #37919

ROTARTSI82 · 2026-04-11T02:51:44Z

-awaiting-author

Co-authored-by: <riccardo.brasca@gmail.com>

…xtensions

Copilot

Pull request overview

This PR generalizes the existing IsAdjoinRootMonic.mkOfAdjoinEqTop construction by adding a new mkOfAdjoinEqTop' that assumes S is a finite free R-module (instead of using integrally-closed hypotheses), and supplies supporting dimension/degree lemmas needed to make the argument work.

Changes:

Add IsAdjoinRootMonic.mkOfAdjoinEqTop' (plus a simp lemma for its root) proving S ≃ₐ[R] AdjoinRoot (minpoly R α) from Algebra.adjoin R {α} = ⊤ under Module.Finite + Module.Free.
Introduce general minpoly degree bounds minpoly.natDegree_le / minpoly.degree_le via Cayley–Hamilton/charpoly of Algebra.lmul.
Add small helper lemmas (OrzechProperty.bijective_of_surjective_of_injective, LinearMap.finrank_le_finrank_of_surjective) and update imports/usages accordingly.

Reviewed changes

Copilot reviewed 11 out of 11 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
Mathlib/RingTheory/IsAdjoinRoot.lean	Adds `mkOfAdjoinEqTop'` and simp lemma, using finrank/OrzechProperty to get bijectivity.
Mathlib/LinearAlgebra/Charpoly/Basic.lean	Refactors variable placement, adjusts `charpoly_natDegree`, and adds `minpoly.(natDegree/degree)_le` via charpoly of `lmul`.
Mathlib/LinearAlgebra/Dimension/Constructions.lean	Adds `LinearMap.finrank_le_finrank_of_surjective`.
Mathlib/RingTheory/OrzechProperty.lean	Adds `bijective_of_surjective_of_injective` helper.
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean	Removes the older field-specific `minpoly.(natDegree/degree)_le` lemmas.
Mathlib/Analysis/Complex/Polynomial/Basic.lean	Updates proof to use the new `minpoly.natDegree_le`.
Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean	Imports charpoly lemma source to keep `minpoly.natDegree_le` available.
Mathlib/FieldTheory/Normal/Basic.lean	Imports charpoly lemma source to keep `minpoly.natDegree_le` available.
Mathlib/FieldTheory/PurelyInseparable/Exponent.lean	Imports charpoly lemma source to keep `minpoly.natDegree_le` available.
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean	Imports charpoly lemma source to keep `minpoly.natDegree_le` available.
Mathlib/RingTheory/Valuation/Minpoly.lean	Imports charpoly lemma source to keep `minpoly.natDegree_le` available.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

riccardobrasca · 2026-04-14T09:21:01Z

            (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 α`.


Can you explain the difference wrt mkOfAdjoinEqTop?

riccardobrasca · 2026-04-14T09:25:23Z

+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
+      (mkOfAdjoinEqTop' hα).root = α := by
+  simp [mkOfAdjoinEqTop', IsAdjoinRoot.root]


Can you add a simp lemma (whose proof will be rfl) that avoids to unfold mkOfAdjoinEqTop' here? Every definition should come with an API (maybe simps can generate it automatically).

I updated the mkOfAdjoinEqTop' definition according to your suggestion, but the mkOfAdjoinEqTop simp lemmas still follow the way I was doing it before (I had just copied the way they did it). Should we update that too in this PR?

If it is just a couple of lines yes please!

riccardobrasca · 2026-04-14T09:28:18Z

Feel free to ignore the comments by copilot if they're nonsense.

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

riccardobrasca · 2026-04-15T19:07:18Z

Thanks!

bors merge

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 α`.

mathlib-bors · 2026-04-15T19:38:26Z

Pull request successfully merged into master.

Build succeeded:

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 10, 2026

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 10, 2026

mathlib-triage Bot assigned dupuisf Mar 16, 2026

ROTARTSI82 and others added 7 commits March 17, 2026 23:33

simp lemma + update mathlib

5a4b075

move lemmas

5823012

Revert "feat(LocalRing/Etale): Finite etale extensions are monogenic"

876313a

This reverts commit cc73956.

oops fix natDegree_le'

e9ccfff

golf away simp lemma

19a085a

ROTARTSI82 force-pushed the grant/monogenic-extensions branch from 2704aea to 19a085a Compare March 18, 2026 06:35

github-actions Bot added the t-ring-theory Ring theory label Mar 21, 2026

dupuisf removed their assignment Apr 1, 2026

mathlib-triage Bot assigned riccardobrasca Apr 2, 2026

bryanboehnke mentioned this pull request Apr 2, 2026

feat(LocalRing/Etale): Finite étale extensions of local rings are monogenic #37527

Open

1 task

artie2000 suggested changes Apr 5, 2026

View reviewed changes

Comment thread Mathlib/FieldTheory/Minpoly/Basic.lean Outdated

Comment thread Mathlib/RingTheory/IsAdjoinRoot.lean Outdated

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 5, 2026

ROTARTSI82 and others added 2 commits April 6, 2026 16:49

use endomorphism cayley-hamilton

d50bc8a

Merge branch 'master' into grant/monogenic-extensions

991e67d

artie2000 suggested changes Apr 7, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

ROTARTSI82 and others added 3 commits April 7, 2026 08:08

Apply suggestions from code review

3ddec91

Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>

golf + fix simpa

00f638a

LinearMap.finrank_le_finrank_of_surjective

b02c2f8

artie2000 reviewed Apr 8, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

ROTARTSI82 and others added 2 commits April 9, 2026 13:04

OrzechProperty.bijective_of_surjective_of_finrank_le

2314a3d

Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>

invoke in mkOfAdjoinEqTop'

821cdc5

artie2000 reviewed Apr 9, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Dimension/Constructions.lean Outdated

artie2000 reviewed Apr 10, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean Outdated

ROTARTSI82 and others added 3 commits April 10, 2026 17:25

unprime minpoly.natDegree_le

11552b2

Merge branch 'master' into grant/monogenic-extensions

d05b4d2

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 11, 2026

riccardobrasca reviewed Apr 13, 2026

View reviewed changes

ROTARTSI82 added 3 commits April 13, 2026 12:57

rm Nontrivial + public import + golf

db4fd80

Co-authored-by: <riccardo.brasca@gmail.com>

missed public import

fedc305

Merge remote-tracking branch 'upstream/master' into grant/monogenic-e…

8ff777a

…xtensions

riccardobrasca requested a review from Copilot April 14, 2026 09:16

Copilot started reviewing on behalf of riccardobrasca April 14, 2026 09:16 View session

Copilot AI reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/LinearAlgebra/Charpoly/Basic.lean

Comment thread Mathlib/RingTheory/IsAdjoinRoot.lean Outdated

riccardobrasca reviewed Apr 14, 2026

View reviewed changes

ROTARTSI82 and others added 2 commits April 14, 2026 10:15

rm another Nontrivial + simp API + golf

c2b0980

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

simp lemmas for mkOfAdjoinEqTop (unprimed)

75af86c

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Apr 15, 2026

mathlib-bors Bot changed the title ~~feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop'~~ [Merged by Bors] - feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' Apr 15, 2026

mathlib-bors Bot closed this Apr 15, 2026

artie2000 mentioned this pull request Apr 17, 2026

[Merged by Bors] - feat: strengthen Cayley-Hamilton #37872

Closed

Conversation

ROTARTSI82 commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Mar 10, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 00dbc4ec64

Import changes for modified files

Declarations diff

Uh oh!

ROTARTSI82 commented Mar 12, 2026

Uh oh!

b-viray commented Mar 21, 2026

Uh oh!

artie2000 commented Apr 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

artie2000 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

artie2000 commented Apr 5, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

artie2000 commented Apr 11, 2026

Uh oh!

ROTARTSI82 commented Apr 11, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

ROTARTSI82 Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

riccardobrasca commented Apr 14, 2026

Uh oh!

riccardobrasca commented Apr 15, 2026

Uh oh!

mathlib-bors Bot commented Apr 15, 2026

Uh oh!

Reviewers

Assignees

ROTARTSI82 commented Mar 10, 2026 •

edited

Loading

github-actions Bot commented Mar 10, 2026 •

edited

Loading

artie2000 commented Apr 5, 2026 •

edited

Loading

artie2000 left a comment •

edited

Loading