feat(RingTheory/Localization): R ⧸ pⁿ ≃+* Rₚ ⧸ (maximalIdeal Rₚ)ⁿ

[wwylele]

This extends the existing def equivQuotMaximalIdeal : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ to powers of maximal ideals.

---

Disclosure of AI usage: I chat with AI for a sketch of the proof. The code is entirely written by me.

I didn't state the simp lemma for the symm direction because I am not sure how to state it. Following the analog of equivQuotMaximalIdeal_symm_apply_mk, this should be

theorem equivQuotMaximalIdealPow_symm_apply_mk (x : R) (s : p.primeCompl) :
    (equivQuotMaximalIdealPow p Rₚ n).symm (Ideal.Quotient.mk _ (IsLocalization.mk' Rₚ x s)) =
        (Ideal.Quotient.mk (p ^ n) x) * (Ideal.Quotient.mk (p ^ n) s)⁻¹ := by

But (Ideal.Quotient.mk (p ^ n) s)⁻¹ is taking inverse in a non-field ring. Here the inverse always exists because s is not in p. What is the mathlib way to say this?

[github-actions]

PR summary f04df22843

Import changes exceeding 2%

%	File
+7.13%	Mathlib.RingTheory.Localization.AtPrime.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Localization.AtPrime.Basic	1220	1307	+87 (+7.13%)

Import changes for all files

Files	Import difference
329 files Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.Ring.EqualizerPushout Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver 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.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.Flat 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.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated 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.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact 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.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.NormalBasis Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.NormalizedTrace Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.SeparablyGenerated Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.ModelTheory.Algebra.Ring.Definability 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.DirichletCharacter.Orthogonality Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZMod 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.MulChar.Duality Mathlib.NumberTheory.Niven 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.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs 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.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.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Finiteness.FinitePresentationLocal Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Ideal.Pure Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.NormalClosure Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.PicardGroup 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.GaussLemma Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Minpoly 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.IncludeLeftSubRight Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.Discrete.RankOne Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Valued.WithVal	1
3 files Mathlib.NumberTheory.LocalField.Basic Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued	3
Mathlib.RingTheory.LocalProperties.ProjectiveDimension Mathlib.RingTheory.LocalProperties.Projective	13
5 files Mathlib.RingTheory.Bialgebra.GroupLike Mathlib.RingTheory.Coalgebra.GroupLike Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.HopfAlgebra.GroupLike	14
Mathlib.RingTheory.LocalProperties.Injective Mathlib.RingTheory.Localization.Free	15
Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.RingHom.FiniteType	24
9 files Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.RingTheory.Finiteness.FiniteTypeLocal Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.RingHom.Bijective Mathlib.RingTheory.RingHom.EssFiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.Surjective	25
Mathlib.RingTheory.LocalRing.ResidueField.Ideal	30
Mathlib.Analysis.Real.Hyperreal Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization	38
3 files Mathlib.Algebra.Order.Ring.StandardPart Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.Localization.Finiteness	39
7 files Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithZeroMulInt	40
Mathlib.RingTheory.SurjectiveOnStalks	70
Mathlib.RingTheory.Localization.AsSubring	78
Mathlib.RingTheory.LocalProperties.Submodule	80
Mathlib.RingTheory.LocalRing.LocalSubring	85
3 files Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Localization.AtPrime.Basic Mathlib.RingTheory.Localization.LocalizationLocalization	87

---

Declarations diff

+ Ideal.Quotient.notMem_of_isUnit_mk_pow
+ coe_subringCongr_apply
+ equivQuotMaximalIdealPow
+ equivQuotMaximalIdealPow_apply_mk
+ subringCongr_symm

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.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
9506	1	backward.isDefEq

Current commit 30443f0b23
Reference commit f04df22843

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