[Merged by Bors] - refactor(IntermediateField/Adjoin): Split off relation to Algebra.adjoin#20630
Closed
[Merged by Bors] - refactor(IntermediateField/Adjoin): Split off relation to Algebra.adjoin#20630
Algebra.adjoin#20630Conversation
PR summary 633ea8fb8b
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.AlgebraicIndependent.Adjoin | 1401 | 1353 | -48 (-3.43%) |
| Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis | 1407 | 1359 | -48 (-3.41%) |
| Mathlib.FieldTheory.SplittingField.IsSplittingField | 1369 | 1374 | +5 (+0.37%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.AlgebraicIndependent.Adjoin |
-48 |
148 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.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.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) |
1351 |
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
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
Vierkantor
approved these changes
Jan 10, 2025
Contributor
Vierkantor
left a comment
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+
Contributor
|
✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Contributor
Author
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 10, 2025
…join` (#20630) Part of `IntermediateField/Adjoin/Basic` is about the relation with `Algebra.adjoin` (e.g., assuming integrality). This PR splits off those results into their own file. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Algebra.adjoinAlgebra.adjoin
grunweg
pushed a commit
that referenced
this pull request
Jan 11, 2025
…join` (#20630) Part of `IntermediateField/Adjoin/Basic` is about the relation with `Algebra.adjoin` (e.g., assuming integrality). This PR splits off those results into their own file. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
Julian
added a commit
that referenced
this pull request
Jan 12, 2025
* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.