switch to Clopens & add lemmas

[alreadydone]

---

[github-actions]

PR summary defbf4ecaf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
470 files Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.CategoryTheory.Abelian.Generator Mathlib.Algebra.Polynomial.Degree.Support Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.BilinearMap Mathlib.Data.Nat.Choose.Cast Mathlib.Algebra.Periodic Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.GroupTheory.Submonoid.Inverses Mathlib.Algebra.BigOperators.Finsupp Mathlib.GroupTheory.CoprodI Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Analysis.Subadditive Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Homology.Opposite Mathlib.Topology.Algebra.UniformField Mathlib.Algebra.Module.Submodule.Invariant Mathlib.LinearAlgebra.SModEq Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Module.Submodule.Basic Mathlib.NumberTheory.Primorial Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.Data.Finsupp.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Data.Finsupp.PWO Mathlib.Logic.Hydra Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Data.Matrix.Composition Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.GroupTheory.DoubleCoset Mathlib.GroupTheory.Perm.Sign Mathlib.Topology.Algebra.Ring.Basic Mathlib.Data.Matrix.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.Data.Matrix.Basis Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.NumberTheory.ArithmeticFunction Mathlib.Topology.Instances.CantorSet Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.RingTheory.TwoSidedIdeal.Operations Mathlib.Algebra.Module.Submodule.Map Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.Data.Real.Sqrt Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.SetTheory.Cardinal.Finsupp Mathlib.Data.Finsupp.Encodable Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.GroupTheory.OrderOfElement Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.Dynamics.OmegaLimit Mathlib.RingTheory.Polynomial.Opposites Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Abelianization Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Preadditive.Generator Mathlib.MeasureTheory.Constructions.AddChar Mathlib.NumberTheory.MulChar.Basic Mathlib.GroupTheory.Exponent Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.GroupTheory.Solvable Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Algebra.Order.Floor.Div Mathlib.Data.Nat.Squarefree Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.AlgebraicGeometry.Noetherian Mathlib.Data.Nat.Factorization.Induction Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.Algebra.Module.Submodule.Range Mathlib.Data.Finsupp.Weight Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.Algebra.Homology.BifunctorFlip Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Homology.TotalComplexShift Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.GroupTheory.Divisible Mathlib.Algebra.MonoidAlgebra.Support Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.GroupTheory.CommutingProbability Mathlib.Topology.MetricSpace.Lipschitz Mathlib.GroupTheory.NoncommPiCoprod Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Polynomial.Inductions Mathlib.Data.Nat.Periodic Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.Algebra.DirectSum.Basic Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.GroupTheory.Coprod.Basic Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Topology.UniformSpace.CompareReals Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Topology.Instances.AddCircle Mathlib.Algebra.Algebra.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.GroupTheory.Perm.Fin Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Topology.Order.Bounded Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Combinatorics.Derangements.Basic Mathlib.Algebra.Category.MonCat.Limits Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Lie.Basic Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.Data.Complex.Exponential Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.NumberTheory.FrobeniusNumber Mathlib.Topology.MetricSpace.Dilation Mathlib.GroupTheory.GroupAction.Period Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Algebra.Hom.Rat Mathlib.GroupTheory.Perm.Option Mathlib.Data.Finsupp.Antidiagonal Mathlib.Algebra.Squarefree.Basic Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Topology.Homotopy.Basic Mathlib.AlgebraicGeometry.Properties Mathlib.Data.ZMod.IntUnitsPower Mathlib.Topology.Instances.Real Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.Topology.Algebra.Equicontinuity Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.RingTheory.Radical Mathlib.RingTheory.Localization.Integer Mathlib.GroupTheory.ClassEquation Mathlib.Topology.Algebra.UniformGroup.Defs Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.AlgebraicTopology.SingularSet Mathlib.Data.Finset.Finsupp Mathlib.RingTheory.Localization.Defs Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.Algebra.UniformMulAction Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.CategoryTheory.Abelian.Refinements Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.SetTheory.Nimber.Field Mathlib.Topology.UniformSpace.Matrix Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Testing.Plausible.Functions Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.Algebra.Polynomial.Coeff Mathlib.CategoryTheory.Monoidal.Tor Mathlib.Algebra.Order.Floor.Prime Mathlib.NumberTheory.SmoothNumbers Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Order.Chebyshev Mathlib.CategoryTheory.Galois.Decomposition Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.Topology.Instances.Rat Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Tactic.ComputeDegree Mathlib.SetTheory.Surreal.Dyadic Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.Geometry.RingedSpace.Basic Mathlib.LinearAlgebra.Pi Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Data.Finsupp.Multiset Mathlib.Algebra.Ring.CentroidHom Mathlib.GroupTheory.FixedPointFree Mathlib.CategoryTheory.Galois.Basic Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Star.CHSH Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.AlgebraicGeometry.AffineSpace Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Star.NonUnitalSubsemiring Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.Computability.TMComputable Mathlib.Data.ZMod.Basic Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.Topology.Algebra.UniformConvergence Mathlib.Algebra.Homology.Monoidal Mathlib.RingTheory.ChainOfDivisors Mathlib.Order.Filter.ENNReal Mathlib.CategoryTheory.Galois.Topology Mathlib.Algebra.Polynomial.Derivative Mathlib.Topology.Algebra.Field Mathlib.Logic.Equiv.TransferInstance Mathlib.Topology.Algebra.UniformRing Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.Data.Nat.Choose.Factorization Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.RingTheory.UniqueFactorizationDomain.Defs Mathlib.GroupTheory.Commensurable Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Topology.UnitInterval Mathlib.NumberTheory.MaricaSchoenheim Mathlib.GroupTheory.Commutator.Finite Mathlib.Data.Real.StarOrdered Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.CategoryTheory.Galois.Full Mathlib.RingTheory.Nilpotent.Basic Mathlib.Algebra.BigOperators.Associated Mathlib.GroupTheory.Index Mathlib.GroupTheory.Perm.Finite Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.CategoryTheory.Localization.Triangulated Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Topology.Algebra.Group.Compact Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Data.ZMod.Units Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.Algebra.Homology.Localization Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.GroupTheory.ArchimedeanDensely Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.Logic.Small.Group Mathlib.SetTheory.Cardinal.Subfield Mathlib.Data.Finsupp.WellFounded Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Combinatorics.Enumerative.Bell Mathlib.Data.Nat.Factorization.Root Mathlib.RingTheory.OreLocalization.Ring Mathlib.Data.ZMod.Factorial Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.DirectSum.AddChar Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Homology.SingleHomology Mathlib.Topology.Connected.PathConnected Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.Algebra.Polynomial.BigOperators Mathlib.Logic.Small.Module Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.GroupTheory.QuotientGroup.Finite Mathlib.Algebra.Category.Ring.Limits Mathlib.Topology.Algebra.Order.UpperLower Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.LinearAlgebra.Span.Defs Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.Finiteness Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.SetTheory.Surreal.Multiplication Mathlib.Data.Nat.Factorization.Basic Mathlib.Topology.Instances.EReal Mathlib.Algebra.DirectSum.Ring Mathlib.Data.Complex.Order Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Group.Subgroup.Finite Mathlib.CategoryTheory.Abelian.Exact Mathlib.Dynamics.Flow Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Homology.QuasiIso Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.Topology.Algebra.GroupCompletion Mathlib.NumberTheory.LucasLehmer Mathlib.AlgebraicGeometry.Stalk Mathlib.RingTheory.Ideal.Prime Mathlib.Algebra.Algebra.ZMod Mathlib.NumberTheory.PrimeCounting Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Star.Subsemiring Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.Data.Nat.Choose.Multinomial Mathlib.Algebra.Module.ZMod Mathlib.CategoryTheory.Galois.Examples Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.RingTheory.Fintype Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.Functor Mathlib.Data.Finsupp.Lex Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.Algebra.Polynomial.Monomial Mathlib.Data.Finsupp.Interval Mathlib.Data.Nat.Factorial.Cast Mathlib.Logic.Equiv.Fintype Mathlib.Algebra.Category.Grp.Biproducts Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.Algebra.Homology.ExactSequence Mathlib.CategoryTheory.Galois.Action Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Topology.Algebra.Localization Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Algebra.Algebra.Equiv Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.RingTheory.SimpleRing.Field Mathlib.GroupTheory.Perm.ConjAct Mathlib.RingTheory.Ideal.Lattice Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.Algebra.CharP.Two Mathlib.Data.Complex.Abs Mathlib.Topology.Algebra.Order.Floor Mathlib.Algebra.Homology.Bifunctor Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Topology.Category.TopCommRingCat Mathlib.Data.Finsupp.AList Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Topology.Homotopy.Equiv Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Algebra.Hom Mathlib.Topology.Homotopy.HSpaces Mathlib.CategoryTheory.Galois.EssSurj Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.CategoryTheory.Linear.Yoneda Mathlib.Topology.Instances.NNReal Mathlib.Algebra.Homology.HomologySequence Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Algebra.Polynomial.Identities Mathlib.Data.Finsupp.Order Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.Polynomial.EraseLead Mathlib.RingTheory.FreeRing Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.LinearAlgebra.FiniteSpan Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Star.CentroidHom Mathlib.Data.DFinsupp.Submonoid Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.Semicontinuous Mathlib.Algebra.Field.Subfield.Basic Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Ring.NegOnePow Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Combinatorics.Derangements.Finite Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.RingTheory.Ideal.BigOperators Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Algebra.Module.Submodule.Ker Mathlib.GroupTheory.Perm.Subgroup Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Data.Nat.Totient Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Topology.Instances.ENNReal Mathlib.GroupTheory.FreeAbelianGroup Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Logic.Small.Ring Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.MeasureTheory.OuterMeasure.BorelCantelli	1
21 files Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC	2

---

Declarations diff

+ DiscreteTopology.of_finite_of_isClosed_singleton
+ IsIdempotentElem.eq_zero_of_isNilpotent
+ RingHom.toLocalizationIsMaximalEquiv
+ RingHom.toLocalizationIsMaximal_surjective_of_discreteTopology
+ _root_.IsIdempotentElem.coe_powers
+ add_sub_mul
+ add_sub_mul_of_commute
+ away_of_isIdempotentElem_of_mul
+ basicOpen_eq_zeroLocus_of_isIdempotentElem
+ basicOpen_injOn_isIdempotentElem
+ basicOpen_isIdempotentElemEquivClopens_symm
+ coe_isIdempotentElemEquivClopens_apply
+ discreteTopology_iff_finite_and_isPrime_imp_isMaximal
+ discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical
+ equivSubtype
+ existsUnique_idempotent_basicOpen_eq_of_isClopen
+ exists_idempotent_basicOpen_eq_of_isClopen
+ exists_le_prime_disjoint
+ exists_le_prime_nmem_of_isIdempotentElem
+ isClopen_iff
+ isClopen_iff_zeroLocus
+ isIdempotentElemEquivClopens
+ isIdempotentElemEquivClopens_apply_toOpens
+ isIdempotentElemEquivClopens_mul
+ isIdempotentElemEquivClopens_one_sub
+ isIdempotentElemEquivClopens_symm_bot
+ isIdempotentElemEquivClopens_symm_compl
+ isIdempotentElemEquivClopens_symm_inf
+ isIdempotentElemEquivClopens_symm_sup
+ isIdempotentElemEquivClopens_symm_top
+ isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton
+ isLocalization_iff_of_isLocalization
+ ker_toSpanSingleton_eq_span
+ ker_toSpanSingleton_one_sub_eq_span
+ of_le_of_exists_dvd
+ quotient_of_isIdempotentElem
+ toLocalizationIsMaximal
+ toLocalizationIsMaximal_injective
+ zeroLocus_eq_basicOpen_of_isIdempotentElem
- PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem
- PrimeSpectrum.isClopen_iff
- PrimeSpectrum.isClopen_iff_zeroLocus
- PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem

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