feat(RingTheory): completion of Gorenstein local ring#41102
Open
Thmoas-Guan wants to merge 991 commits into
Open
feat(RingTheory): completion of Gorenstein local ring#41102Thmoas-Guan wants to merge 991 commits into
Thmoas-Guan wants to merge 991 commits into
Conversation
…on-in-LinearEquiv
…on-in-LinearEquiv
github-actions
Bot
added
large-import
PR summary 0fdad71e77Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.AdicCompletion.Noetherian | 1877 | 2290 | +413 (+22.00%) |
| Mathlib.Algebra.Module.FinitePresentation | 1372 | 1468 | +96 (+7.00%) |
| Mathlib.RingTheory.ReesAlgebra | 1388 | 1422 | +34 (+2.45%) |
Import changes for all files
| Files | Import difference |
|---|---|
81 filesMathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.IntermediateField Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.RatFunc.Valuation Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum 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.Complex Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure 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.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Inertia Mathlib.NumberTheory.RamificationInertia.Valuation Mathlib.NumberTheory.RatFunc.Ostrowski Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.OrderOfVanishing.Noetherian 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.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic |
1 |
25 filesMathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.EtalePoint Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.RingTheory.Etale.Descent Mathlib.RingTheory.Etale.Finite Mathlib.RingTheory.Etale.Weakly Mathlib.RingTheory.LocalRing.Etale Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.TotallySplit Mathlib.RingTheory.Unramified.LocalStructure |
2 |
83 filesMathlib.Algebra.Module.StablyFree.FreeOfInvertible Mathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite 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.NumberTheory.FLT.Three Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Cyclotomic.Basic 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.Different Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Ramification Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.Flat.Rank Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RamificationInertia.Basic Mathlib.RingTheory.RamificationInertia.Ramification Mathlib.RingTheory.Regular.ProjectiveDimension Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Quotient Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.ZariskisMainTheorem Mathlib.Topology.Algebra.Ring.Compact |
3 |
16 filesMathlib.RingTheory.Depth.Rees Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Extension.Cotangent.BaseChange Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.LinearMap Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Unramified.Dedekind Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Locus |
4 |
3 filesMathlib.RingTheory.Extension.ExtendScalars Mathlib.RingTheory.Extension.Generators Mathlib.RingTheory.Kaehler.JacobiZariski |
5 |
8 filesMathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.RingTheory.Ideal.CotangentBaseChange Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.RegularLocalRing.Defs Mathlib.RingTheory.RegularLocalRing.Polynomial |
6 |
Mathlib.Algebra.Module.SpanRankOperations Mathlib.RingTheory.AdicCompletion.LocalRing |
8 |
Mathlib.RingTheory.Extension.Basic |
9 |
Mathlib.RingTheory.AdicCompletion.AsTensorProduct |
11 |
Mathlib.RingTheory.LocalProperties.InjectiveDimension Mathlib.RingTheory.LocalProperties.ProjectiveDimension |
12 |
3 filesMathlib.NumberTheory.NumberField.Completion.Ramification Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.QuasiFinite.Polynomial |
13 |
Mathlib.RingTheory.RamificationInertia.Inertia |
15 |
10 filesMathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.QuasiFinite.Weakly Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent |
16 |
4 filesMathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.LocalProperties.Injective Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.Localization.Free |
17 |
Mathlib.RingTheory.Extension.Cotangent.Free |
18 |
3 filesMathlib.Algebra.Module.Presentation.Differentials Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Smooth.Kaehler |
19 |
Mathlib.RingTheory.Ideal.Cotangent |
22 |
Mathlib.RingTheory.AdicCompletion.Exactness |
30 |
Mathlib.RingTheory.Filtration Mathlib.RingTheory.ReesAlgebra |
34 |
Mathlib.RingTheory.LocalProperties.FinitePresentation |
68 |
Mathlib.RingTheory.Regular.Free |
80 |
Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite |
96 |
Mathlib.RingTheory.AdicCompletion.Noetherian |
413 |
Mathlib.Algebra.Category.ModuleCat.Ext.RingEquiv (new file) |
1723 |
Mathlib.Algebra.Category.ModuleCat.Ext.Baer (new file) |
1942 |
Mathlib.Algebra.Category.ModuleCat.InjectiveDimension (new file) |
1978 |
Mathlib.Algebra.Category.ModuleCat.Ext.BaseChange (new file) |
1986 |
Mathlib.RingTheory.Gorenstein.Defs (new file) |
2044 |
Mathlib.RingTheory.Regular.InjectiveDimension (new file) |
2415 |
Mathlib.RingTheory.Gorenstein.Completion (new file) |
2541 |
Declarations diff (regex)
+ AdicCompletion.isNoetherianRing_of_fg
+ AdicCompletion.ringKrullDim_eq
+ CategoryTheory.Abelian.Ext.isBaseChange_aux
+ Ext.isBaseChange
+ Ext.isBaseChangeMap
+ Ext.isBaseChangeMapAux
+ Ext.isLocalizedModule
+ Ext.isLocalizedModuleMap
+ ExtendScalars'.map'
+ ExtendScalars'.map'_comp
+ ExtendScalars'.map'_id
+ ExtendScalars'.obj'
+ Function.Bijective.subsingleton_congr
+ Ideal.toAssociatedGraded
+ IsGorensteinLocalRing
+ IsGorensteinLocalRing.iff_adicCompletion
+ IsGorensteinLocalRing.of_ringEquiv
+ IsGorensteinRing
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ Module.FinitePresentation.exists_fin'
+ Module.FinitePresentation.isBaseChange_map
+ Module.isBaseChange_map_of_finite_free
+ ModuleCat.extendScalars'.mapExtLinearMap
+ ModuleCat.extendScalars'.mapExtLinearMap_eq_mapExt
+ ModuleCat.extendScalars'.mapLinearMap
+ ModuleCat.extendScalars'.mapLinearMap_eq_mapAddHom
+ ModuleCat.isBaseChange_hom
+ ModuleCat.isoExtendScalars'OfIsBaseChange'
+ ModuleCat.restrictScalarsFullyFaithfulOfSurjective
+ exist_nat_eq'
+ exists_coeffs_sub_mem
+ exists_monomial_span_of_fg
+ extClass_comp_mapExt_bijective
+ extClass_postcomp_bijective_of_isSMulRegular
+ extQuotientBotZeroEquiv
+ extRestrictScalarsSemiLinearEquiv
+ extRestrictScalarsSemiLinearMap
+ extRestrictScalarsSemiLinearMap_toAddMonoidHom
+ extSemiLinearEquivOfSemiLinearEquiv
+ ext_quotient_one_subsingleton_iff
+ ext_residueField_subsingleton_iff
+ ext_subsingleton_of_all_gt
+ ext_subsingleton_of_support_subset
+ ext_vanish_of_residueField_vanish
+ extendScalars'
+ extendScalars'_map_exact
+ finite_QuotSMulTop'
+ hasInjectiveDimensionLE_of_quotients
+ hasInjectiveDimensionLT_iff_quotients
+ hasInjectiveDimensionLT_of_quotients
+ hasInjectiveDimensionLT_of_semiLinearEquiv
+ hasProjectiveDimensionLE_finsupp_quotient_regular
+ injectiveDimension_eq_of_semiLinearEquiv
+ injectiveDimension_eq_sInf_of_finite
+ injectiveDimension_lt_iff_of_finite
+ injectiveDimension_quotSMulTop_succ_eq_injectiveDimension
+ injective_iff_subsingleton_ext_quotient_one
+ injective_of_subsingleton_ext_quotient_one
+ instance (M N : ModuleCat.{v'} S) : IsScalarTower R S (M ⟶ N)
+ instance (M N : ModuleCat.{v'} S) : Module R (M ⟶ N)
+ instance (M N : Type*) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : IsScalarTower R S (Ext M N n)
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : Module R (Ext M N n)
+ instance : (extendScalars' R S).Additive
+ instance [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion I R)
+ instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by
+ isBaseChange_adicCompletion_subsingleton_iff
+ isGorensteinLocalRing_def
+ isGorensteinLocalRing_iff_exists'
+ isGorensteinRing_def
+ isGorensteinRing_def'
+ isGorensteinRing_of_ringEquiv
+ isNoetherianRing_of_isAdicComplete_of_fg
+ isNoetherianRing_reesAlgebra_quotient
+ isoRestrictScalars
+ mem_map_algebraMap_reesAlgebra_iff
+ one_subsingleton_iff_of_projective
+ quotientIsBaseChangeMap'
+ quotientIsBaseChangeMap'_isBaseChange
+ reesAlgebraToAssociatedGraded
+ subsingleton_of_ext_quotient_bot_zero
+ tensorProduct_reesAlgebra_isNoetherian_of_fg
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
0fdad71).
- +98 new declarations
- −0 removed declarations
+AdicCompletion.isNoetherianRing_of_fg
+AdicCompletion.ringKrullDim_eq
+CategoryTheory.Abelian.Ext.isBaseChange
+CategoryTheory.Abelian.Ext.isBaseChangeMap
+CategoryTheory.Abelian.Ext.isBaseChangeMapAux
+CategoryTheory.Abelian.Ext.isBaseChange_aux
+CategoryTheory.Abelian.Ext.isLocalizedModule
+CategoryTheory.Abelian.Ext.isLocalizedModuleMap
+CategoryTheory.Abelian.Ext.one_subsingleton_iff_of_projective
+CategoryTheory.Abelian.extFunctorObj.congr_simp
+CategoryTheory.hasInjectiveDimensionLT_of_semiLinearEquiv
+CategoryTheory.injectiveDimension_eq_of_semiLinearEquiv
+Function.Bijective.subsingleton_congr
+Ideal.toAssociatedGraded
+IsGorensteinLocalRing
+IsGorensteinLocalRing.casesOn
+IsGorensteinLocalRing.iff_adicCompletion
+IsGorensteinLocalRing.injdim
+IsGorensteinLocalRing.mk
+IsGorensteinLocalRing.of_ringEquiv
+IsGorensteinLocalRing.rec
+IsGorensteinLocalRing.recOn
+IsGorensteinLocalRing.toIsLocalRing
+IsGorensteinRing
+IsGorensteinRing.casesOn
+IsGorensteinRing.isGorenstein_localize
+IsGorensteinRing.mk
+IsGorensteinRing.rec
+IsGorensteinRing.recOn
+IsLocalRing.ResidueField.map_bijective_of_surjective
+Module.FinitePresentation.exists_fin'
+Module.FinitePresentation.isBaseChange_map
+Module.isBaseChange_map_of_finite_free
+ModuleCat.Algebra'.extendScalars'_linear
+ModuleCat.ExtendScalars'.map'
+ModuleCat.ExtendScalars'.map'_comp
+ModuleCat.ExtendScalars'.map'_id
+ModuleCat.ExtendScalars'.obj'
+ModuleCat.extRestrictScalarsSemiLinearEquiv
+ModuleCat.extRestrictScalarsSemiLinearMap
+ModuleCat.extRestrictScalarsSemiLinearMap_toAddMonoidHom
+ModuleCat.extSemiLinearEquivOfSemiLinearEquiv
+ModuleCat.ext_quotient_one_subsingleton_iff
+ModuleCat.extendScalars'
+ModuleCat.extendScalars'.congr_simp
+ModuleCat.extendScalars'.mapExtLinearMap
+ModuleCat.extendScalars'.mapExtLinearMap.congr_simp
+ModuleCat.extendScalars'.mapExtLinearMap_eq_mapExt
+ModuleCat.extendScalars'.mapLinearMap
+ModuleCat.extendScalars'.mapLinearMap_eq_mapAddHom
+ModuleCat.extendScalars'_map_exact
+ModuleCat.hasInjectiveDimensionLE_of_quotients
+ModuleCat.hasInjectiveDimensionLT_iff_quotients
+ModuleCat.hasInjectiveDimensionLT_of_quotients
+ModuleCat.injective_iff_subsingleton_ext_quotient_one
+ModuleCat.injective_of_subsingleton_ext_quotient_one
+ModuleCat.instAdditiveExtendScalars'
+ModuleCat.instPreservesFiniteColimitsExtendScalars'OfFlat
+ModuleCat.instPreservesFiniteLimitsExtendScalars'OfFlat
+ModuleCat.instSmallTensorProduct
+ModuleCat.isBaseChange_hom
+ModuleCat.isoExtendScalars'OfIsBaseChange'
+ModuleCat.isoExtendScalars'OfIsBaseChange'.congr_simp
+ModuleCat.isoRestrictScalars
+ModuleCat.restrictScalarsFullyFaithfulOfSurjective
+ModuleCat.shortComplexOfConj.congr_simp
+exist_nat_eq'
+exists_coeffs_sub_mem
+exists_monomial_span_of_fg
+extClass_comp_mapExt_bijective
+extClass_postcomp_bijective_of_isSMulRegular
+ext_residueField_subsingleton_iff
+ext_subsingleton_of_all_gt
+ext_subsingleton_of_support_subset
+ext_vanish_of_residueField_vanish
+finite_QuotSMulTop'
+hasProjectiveDimensionLE_finsupp_quotient_regular
+injectiveDimension_eq_sInf_of_finite
+injectiveDimension_lt_iff_of_finite
+injectiveDimension_quotSMulTop_succ_eq_injectiveDimension
+instIsNoetherianRingAdicCompletion
+instIsScalarTowerExtModuleCat
+instIsScalarTowerHomModuleCat
+instModuleExtModuleCat
+instModuleHomModuleCat
+isBaseChange_adicCompletion_subsingleton_iff
+isGorensteinLocalRing_def
+isGorensteinLocalRing_iff_exists'
+isGorensteinRing_def
+isGorensteinRing_def'
+isGorensteinRing_of_ringEquiv
+isNoetherianRing_of_isAdicComplete_of_fg
+isNoetherianRing_reesAlgebra_quotient
+mem_map_algebraMap_reesAlgebra_iff
+quotientIsBaseChangeMap'
+quotientIsBaseChangeMap'_isBaseChange
+reesAlgebraToAssociatedGraded
+tensorProduct_reesAlgebra_isNoetherian_of_fgIncrease in strong tech debt: (relative, absolute) = (8.67, 0.00)
| Current number | Change | Type (strong) |
|---|---|---|
| 4517 | 2 | backward.defeqAttrib.useBackward |
| 5644 | 17 | backward.isDefEq.respectTransparency |
Increase in weak tech debt: (relative, absolute) = (6.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 5008 | 6 | exposed public sections |
Current commit 0fdad71e77
Reference commit 1c3e8f34a8
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).
4 tasks
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
…on-in-LinearEquiv
…on-of-quotSMulTop
…al-Ring-completion
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
2 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.
In this PR, we proved a Noetherian local ring is Gorenstein iff its completion is.
Extcommute with flat base change #33369