refactor(IntermediateField/Adjoin): Split off relation to Algebra.adjoin
#20630
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PR summary 3fd0ab8a41
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.AlgebraicIndependent.Adjoin | 1399 | 1351 | -48 (-3.43%) |
| Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis | 1405 | 1357 | -48 (-3.42%) |
| Mathlib.FieldTheory.SplittingField.IsSplittingField | 1367 | 1372 | +5 (+0.37%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.AlgebraicIndependent.Adjoin |
-48 |
150 filesMathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.FieldTheory.IsPerfectClosure Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.GaussSum Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.RingTheory.Localization.NormTrace Mathlib.FieldTheory.AbelRuffini Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.NumberTheory.NumberField.Norm Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.FieldTheory.Isaacs Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.RingTheory.Trace.Basic Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.FieldTheory.Normal Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Algebra.Lie.Derivation.Killing Mathlib.FieldTheory.SeparableClosure Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.Analysis.Fourier.ZMod Mathlib.RingTheory.Invariant Mathlib.NumberTheory.Cyclotomic.Three Mathlib.RingTheory.Unramified.Field Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.RingTheory.Nullstellensatz Mathlib.NumberTheory.NumberField.Completion Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Fixed Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Algebra.Lie.TraceForm Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.FieldTheory.Extension Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.RingTheory.Etale.Field Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.RepresentationTheory.Invariants Mathlib.FieldTheory.KrullTopology Mathlib.Algebra.Lie.LieTheorem Mathlib.CategoryTheory.Preadditive.Schur Mathlib.FieldTheory.Relrank Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.LinearDisjoint Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.FieldTheory.Finite.GaloisField Mathlib.RepresentationTheory.Character Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.NumberTheory.FLT.Three Mathlib.FieldTheory.Galois.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.Algebra.Lie.Weights.Chain Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.FieldTheory.PrimitiveElement Mathlib.NumberTheory.Fermat Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.FieldTheory.AlgebraicClosure Mathlib.NumberTheory.NumberField.Basic Mathlib.FieldTheory.CardinalEmb Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.Analysis.Normed.Algebra.Basic Mathlib.RepresentationTheory.FDRep Mathlib.RingTheory.WittVector.Isocrystal Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Polynomial.Selmer Mathlib.FieldTheory.NormalClosure Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.Algebra.Lie.Weights.Killing Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.FieldTheory.KummerExtension Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.FieldTheory.JacobsonNoether Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.FieldTheory.PurelyInseparable Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Algebra.Lie.Weights.Cartan Mathlib.RingTheory.Valuation.Minpoly Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.FieldTheory.Galois.Infinite Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.AxGrothendieck Mathlib.Tactic Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.RingTheory.Norm.Basic Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.NumberField.AdeleRing |
1 |
23 filesMathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Identities Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Semisimple Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.FieldTheory.Perfect Mathlib.NumberTheory.KummerDedekind Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.FieldTheory.PerfectClosure Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.FieldTheory.SplittingField.Construction Mathlib.RingTheory.Perfection |
4 |
Mathlib.FieldTheory.SplittingField.IsSplittingField |
5 |
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (new file) |
1349 |
Declarations diff
+ IntermediateField.adjoin_rootSet_isSplittingField
+ IntermediateField.isSplittingField_iff
+ isSplittingField_iff_intermediateField
- _root_.isSplittingField_iff_intermediateField
- adjoin_rootSet_isSplittingField
- isSplittingField_iff
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Ruben-VandeVelde
approved these changes
Jan 10, 2025
| /-! | ||
| # Adjoining Elements to Fields | ||
| This file relates `IntermediateField.Adjoin` to `Algebra.adjoin`. |
There was a problem hiding this comment.
Suggested change
| This file relates `IntermediateField.Adjoin` to `Algebra.adjoin`. | |
| This file relates `IntermediateField.adjoin` to `Algebra.adjoin`. |
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
Vierkantor
approved these changes
Jan 10, 2025
There was a problem hiding this comment.
I had noted before that IntermediateField.Adjoin could stand some cleaning up, thank you for taking this on!
I think the extra imports in IsSplittingField are okay. I don't think it would help right now, but at some point we can consider taking out all the IntermediateField results from that file, and then this would not matter at all.
bors d+
|
✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Part of
IntermediateField/Adjoin/Basicis about the relation withAlgebra.adjoin(e.g., assuming integrality). This PR splits off those results into their own file.