Feat: add `PowerBasis.exists_sModEq`

[riccardobrasca]

We add PowerBasis.exists_sModEq.

From flt-regular.

---

[github-actions[bot]]

PR summary 8726c43b8c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.PowerBasis	1189	1190	+1 (+0.08%)

Import changes for all files

Files

Import difference

134 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.RingTheory.IsAdjoinRoot Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.Complex.Polynomial Mathlib.FieldTheory.IsPerfectClosure Mathlib.NumberTheory.Wilson Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.PowerBasis Mathlib.FieldTheory.Finite.Trace Mathlib.RingTheory.WittVector.Domain Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.Localization.NormTrace Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.NumberTheory.NumberField.Norm Mathlib.FieldTheory.Galois Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.WittVector.MulCoeff Mathlib.FieldTheory.Normal Mathlib.Analysis.NormedSpace.Star.GelfandDuality Mathlib.RingTheory.WittVector.Identities Mathlib.FieldTheory.Adjoin Mathlib.Algebra.Lie.Derivation.Killing Mathlib.FieldTheory.SeparableClosure Mathlib.RingTheory.WittVector.Truncated Mathlib.LinearAlgebra.JordanChevalley Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.RingTheory.Nullstellensatz Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.FieldTheory.Fixed Mathlib.RingTheory.Adjoin.Field Mathlib.FieldTheory.Finite.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.Analysis.NormedSpace.Spectrum Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Extension Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus Mathlib.RepresentationTheory.Invariants Mathlib.FieldTheory.KrullTopology Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.NormedSpace.Star.Spectrum Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.FieldTheory.Finite.GaloisField Mathlib.RepresentationTheory.Character Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.Analysis.NormedSpace.Algebra Mathlib.RingTheory.WittVector.Verschiebung Mathlib.Algebra.Lie.Weights.Chain Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.FieldTheory.PrimitiveElement Mathlib.RingTheory.Smooth.Basic Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Discriminant Mathlib.NumberTheory.SumTwoSquares Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.NumberTheory.ClassNumber.Finite Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Mathport.Syntax Mathlib.FieldTheory.Cardinality Mathlib.RingTheory.IntegralRestrict Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.NumberTheory.KummerDedekind Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Order Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.RingTheory.WittVector.Frobenius Mathlib.NumberTheory.NumberField.Basic Mathlib.RingTheory.WittVector.Basic Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict Mathlib.RepresentationTheory.FDRep Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Unramified.Basic Mathlib.FieldTheory.NormalClosure Mathlib.NumberTheory.FermatPsp Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.RingTheory.AdjoinRoot Mathlib.Algebra.Lie.Weights.Killing Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.FieldTheory.KummerExtension Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Topology.ContinuousFunction.UniqueCFC Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.FieldTheory.PurelyInseparable Mathlib.RingTheory.WittVector.IsPoly Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.RingTheory.WittVector.Defs Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.FieldTheory.PerfectClosure Mathlib.Algebra.Polynomial.Bivariate Mathlib.RingTheory.Unramified.Derivations Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.SplittingField.Construction Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.RingTheory.Perfection Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.WittVector.MulP

1

---

Declarations diff

+ exists_gen_dvd_sub + exists_smodEq

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>

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9201f1e545b55d209b241c8808a5c47da76bd893. There were no significant changes against commit 4d0428ba5998dacfc296847343a8d237674182e5.

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

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

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style