[Merged by Bors] - chore: redefine AlgEquiv.refl with RingEquiv.refl by Ruben-VandeVelde · Pull Request #18856 · leanprover-community/mathlib4

Ruben-VandeVelde · 2024-11-11T10:30:39Z

Using 1 requires an unnecessary import.

github-actions · 2024-11-11T10:31:30Z

PR summary 1b11289dcb

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Algebra.Equiv	687	686	-1 (-0.15%)

Import changes for all files

Files	Import difference
390 files `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Abelian.Generator` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.RingTheory.AlgebraTower` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Data.Matrix.Composition` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.Category.Grp.AB5` `Mathlib.Data.Matrix.Basic` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Data.Matrix.PEquiv` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.CategoryTheory.Preadditive.Generator` `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.CategoryTheory.Abelian.ProjectiveResolution` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Analysis.Convex.Slope` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.Data.Matrix.CharP` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Group.AddChar` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.Algebra.Module.LocalizedModule.Basic` `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.Algebra.Pi` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.CategoryTheory.Abelian.Injective` `Mathlib.Analysis.Convex.Join` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.CategoryTheory.Abelian.Projective` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Module.LocalizedModule.IsLocalization` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.LinearAlgebra.LinearIndependent` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.RingTheory.Binomial` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.Logic.Equiv.TransferInstance` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.DirectLimit` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.CategoryTheory.Galois.Full` `Mathlib.LinearAlgebra.Ray` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.Analysis.Convex.Mul` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.CategoryTheory.Triangulated.Opposite` `Mathlib.Analysis.Convex.Segment` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.Algebra.Module.Injective` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.Topology.Algebra.Algebra` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.Logic.Small.Group` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.Logic.Small.Module` `Mathlib.RingTheory.Localization.Basic` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.Algebra.Category.AlgebraCat.Monoidal` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.Analysis.Convex.Function` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.CategoryTheory.Preadditive.ProjectiveResolution` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Algebra.Category.AlgebraCat.Basic` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.Tactic.Module` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.Idempotents` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Analysis.Convex.Strict` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Central.Basic` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Star` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Analysis.Convex.Basic` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.CategoryTheory.Abelian.InjectiveResolution` `Mathlib.Algebra.CharP.Algebra` `Mathlib.RingTheory.Localization.Module` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.CategoryTheory.Preadditive.InjectiveResolution` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Analysis.Convex.Extreme` `Mathlib.CategoryTheory.Galois.Action` `Mathlib.Data.Matrix.DualNumber` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.LinearAlgebra.TensorPower` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.Algebra.Algebra.Tower` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Tactic.Algebraize` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.FreeAlgebra` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Analysis.Convex.Exposed` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Logic.Small.Ring` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.Topology.Algebra.ContinuousMonoidHom`	-1

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

grunweg

LGTM, thanks!
maintainer merge

github-actions · 2024-11-11T11:06:54Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

github-actions · 2024-11-11T11:06:54Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

Vierkantor

Nicely spotted!

bors r+

Using `1` requires an unnecessary import.

mathlib-bors · 2024-11-11T11:38:32Z

Pull request successfully merged into master.

Build succeeded:

Using `1` requires an unnecessary import.

chore: redefine AlgEquiv.refl with RingEquiv.refl

1b11289

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Nov 11, 2024

grunweg reviewed Nov 11, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 11, 2024

Vierkantor approved these changes Nov 11, 2024

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Nov 11, 2024

mathlib-bors bot pushed a commit that referenced this pull request Nov 11, 2024

chore: redefine AlgEquiv.refl with RingEquiv.refl (#18856)

ba0f793

Using `1` requires an unnecessary import.

mathlib-bors bot changed the title ~~chore: redefine AlgEquiv.refl with RingEquiv.refl~~ [Merged by Bors] - chore: redefine AlgEquiv.refl with RingEquiv.refl Nov 11, 2024

mathlib-bors bot closed this Nov 11, 2024

mathlib-bors bot deleted the AlgEquiv.refl branch November 11, 2024 11:38

Jun2M pushed a commit that referenced this pull request Nov 17, 2024

chore: redefine AlgEquiv.refl with RingEquiv.refl (#18856)

949f099

Using `1` requires an unnecessary import.

TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024

chore: redefine AlgEquiv.refl with RingEquiv.refl (#18856)

e0d09c2

Using `1` requires an unnecessary import.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: redefine AlgEquiv.refl with RingEquiv.refl#18856

[Merged by Bors] - chore: redefine AlgEquiv.refl with RingEquiv.refl#18856
Ruben-VandeVelde wants to merge 1 commit intomasterfrom
AlgEquiv.refl

Ruben-VandeVelde commented Nov 11, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 11, 2024

Import changes for modified files

Uh oh!

grunweg left a comment

Uh oh!

github-actions bot commented Nov 11, 2024

Uh oh!

github-actions bot commented Nov 11, 2024

Uh oh!

Vierkantor left a comment

Uh oh!

mathlib-bors bot commented Nov 11, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Ruben-VandeVelde commented Nov 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 11, 2024

PR summary 1b11289dcb

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 11, 2024

Uh oh!

github-actions bot commented Nov 11, 2024

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Nov 11, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Ruben-VandeVelde commented Nov 11, 2024 •

edited

Loading