Skip to content

[Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers#29277

Closed
wwylele wants to merge 2 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn-zpos
Closed

[Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers#29277
wwylele wants to merge 2 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn-zpos

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented Sep 3, 2025

Part of #29275. I put it immediately under IsLocalization (nonZeroDivisors ℤ) ℚ given the similarity.

Open in Gitpod

@wwylele wwylele mentioned this pull request Sep 3, 2025
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 3, 2025 •
edited
Loading

PR summary 1c58764af6

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.Localization.FractionRing 951 952 +1 (+0.11%)
Import changes for all files
Files Import difference
490 files Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.CharP.Subring Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Module.Presentation.Finite Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.MvPolynomial.Nilpotent Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.Homogenize Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.IdealSheaf Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.Polynomial.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.Nullstellensatz Mathlib.Data.Nat.PowModTotient Mathlib.Data.Real.GoldenRatio Mathlib.Data.Real.Irrational Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Differential.Basic Mathlib.FieldTheory.Differential.Liouville Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Finite.Basic Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.Galois.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.IsSepClosed Mathlib.FieldTheory.Isaacs Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.KrullTopology Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Minpoly.ConjRootClass Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.FieldTheory.Normal.Basic Mathlib.FieldTheory.Normal.Closure Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.PrimitiveElement Mathlib.FieldTheory.PurelyInseparable.Basic Mathlib.FieldTheory.PurelyInseparable.Exponent Mathlib.FieldTheory.PurelyInseparable.PerfectClosure Mathlib.FieldTheory.RatFunc.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.Vandermonde Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Pell Mathlib.NumberTheory.Rayleigh Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.SumTwoSquares Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.CotangentLocalizationAway Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.EisensteinCriterion Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Inverse Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.NoetherNormalization Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Polynomial.ContentIdeal Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Criterion Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.Eisenstein.Generalized Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.Polynomial.SmallDegreeVieta Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.PowerSeries.WeierstrassPreparation Mathlib.RingTheory.Presentation Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.IntegrallyClosed Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValExtension Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Complete Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.Isocrystal Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.Tactic.NormNum.Irrational Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithZeroMulInt Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.Instances.AddCircle.DenseSubgroup Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.RatLemmas
 1

Declarations diff

+ instance : IsLocalization (Submonoid.pos ℤ) ℚ

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

@github-actions github-actions bot added the t-ring-theory Ring theory label Sep 3, 2025
vihdzp
vihdzp approved these changes Sep 3, 2025
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Sep 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks fine with @vihdzp's suggestion (assuming it works).

Note that it adds one import to 490 modules; this might be fine.

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 3, 2025

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 3, 2025
jcommelin
jcommelin reviewed Sep 4, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Sep 4, 2025
mathlib-bors bot pushed a commit that referenced this pull request Sep 4, 2025
@wwylele
feat(RingTheory): Rat is localization of Int at positive integers (#2…
896dbda 
…9277)

Part of #29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 4, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory): Rat is localization of Int at positive integers [Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers Sep 4, 2025
@mathlib-bors mathlib-bors bot closed this Sep 4, 2025
@wwylele wwylele deleted the wwylele-hahn-zpos branch September 4, 2025 12:42
CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele @CBirkbeck
feat(RingTheory): Rat is localization of Int at positive integers (le…
1df7433 
…anprover-community#29277)

Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.
yuanyi-350 pushed a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025
@wwylele @yuanyi-350
feat(RingTheory): Rat is localization of Int at positive integers (le…
154b023 
…anprover-community#29277)

Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.
robertmaxton42 pushed a commit to robertmaxton42/mathlib4 that referenced this pull request Sep 11, 2025
@wwylele @robertmaxton42
feat(RingTheory): Rat is localization of Int at positive integers (le…
a3d9ec9 
…anprover-community#29277)

Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@wwylele @joelriou
feat(RingTheory): Rat is localization of Int at positive integers (le…
963348e 
…anprover-community#29277)

Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

+1 more reviewer

@vihdzp vihdzp vihdzp approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@wwylele @jcommelin @vihdzp @Ruben-VandeVelde