[Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete #15806

YaelDillies · 2024-08-14T10:36:52Z

All lemmas can be moved to earlier files

github-actions · 2024-08-14T10:37:31Z

PR summary 3b3f0ba668

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.GroupAction.Group	367	0	-367 (-100.00%)
Mathlib.Algebra.GroupWithZero.Action.Defs	179	202	+23 (+12.85%)
Mathlib.Algebra.GroupWithZero.Action.Units	196	203	+7 (+3.57%)
Mathlib.Algebra.GroupWithZero.Action.Prod	205	211	+6 (+2.93%)
Mathlib.Algebra.Order.Module.Defs	459	448	-11 (-2.40%)
Mathlib.Algebra.Module.Basic	425	420	-5 (-1.18%)
Mathlib.Data.Set.Pointwise.SMul	422	421	-1 (-0.24%)
Mathlib.Algebra.Order.Module.OrderedSMul	481	480	-1 (-0.21%)
Mathlib.GroupTheory.GroupAction.Basic	549	548	-1 (-0.18%)
Mathlib.Data.Finsupp.Basic	657	656	-1 (-0.15%)

Import changes for all files

Files	Import difference
`Mathlib.GroupTheory.GroupAction.Group`	-367
`Mathlib.Algebra.Order.Module.Defs`	-11
`Mathlib.Algebra.Module.Basic`	-5
139 files `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology` `Mathlib.Topology.Order.LawsonTopology` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.Topology.CompactOpen` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.CategoryTheory.Sites.Coherent.Comparison` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Topology.Algebra.Order.Compact` `Mathlib.Topology.Compactification.OnePoint` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.Topology.UniformSpace.Ascoli` `Mathlib.Topology.UniformSpace.Compact` `Mathlib.Topology.Sheaves.Sheaf` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.Topology.Sets.Closeds` `Mathlib.Topology.Order.ScottTopology` `Mathlib.Topology.ExtremallyDisconnected` `Mathlib.Topology.Category.TopCat.EpiMono` `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi` `Mathlib.CategoryTheory.Sites.EpiMono` `Mathlib.Topology.UniformSpace.CompactConvergence` `Mathlib.Algebra.Order.Module.Algebra` `Mathlib.Topology.LocalAtTarget` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular` `Mathlib.Topology.LocallyConstant.Basic` `Mathlib.Topology.ContinuousFunction.CocompactMap` `Mathlib.Topology.Order.Hom.Esakia` `Mathlib.Topology.Baire.LocallyCompactRegular` `Mathlib.Topology.Spectral.Hom` `Mathlib.CategoryTheory.Sites.InducedTopology` `Mathlib.Topology.PartialHomeomorph` `Mathlib.Topology.ClopenBox` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.Topology.Sequences` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Order.LowerUpperTopology` `Mathlib.Topology.UniformSpace.AbstractCompletion` `Mathlib.Topology.Category.TopCat.Basic` `Mathlib.Topology.Maps.Proper.Basic` `Mathlib.Topology.Sober` `Mathlib.Topology.UniformSpace.CompleteSeparated` `Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves` `Mathlib.Topology.Category.TopCat.Limits.Cofiltered` `Mathlib.Algebra.Order.Module.Rat` `Mathlib.Topology.Homeomorph` `Mathlib.Combinatorics.SimpleGraph.Ends.Defs` `Mathlib.CategoryTheory.Sites.Coherent.Basic` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.Topology.Gluing` `Mathlib.Topology.Sets.Order` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.Topology.Hom.Open` `Mathlib.Topology.ContinuousFunction.Basic` `Mathlib.Topology.Category.TopCat.OpenNhds` `Mathlib.Combinatorics.SimpleGraph.Finsubgraph` `Mathlib.Topology.ContinuousFunction.Ordered` `Mathlib.Topology.Category.CompHausLike.Basic` `Mathlib.CategoryTheory.Sites.LeftExact` `Mathlib.Topology.NoetherianSpace` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.Topology.Category.TopCat.Opens` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.Topology.Covering` `Mathlib.Topology.UniformSpace.UniformEmbedding` `Mathlib.CategoryTheory.Sites.Spaces` `Mathlib.Topology.UniformSpace.Completion` `Mathlib.Topology.Category.TopCat.Limits.Konig` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Topology.Sheaves.Limits` `Mathlib.Topology.ContinuousFunction.Sigma` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.Topology.Specialization` `Mathlib.Topology.Order.UpperLowerSetTopology` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.Topology.UniformSpace.UniformConvergence` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves` `Mathlib.Topology.Algebra.Constructions` `Mathlib.Topology.UniformSpace.Cauchy` `Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology` `Mathlib.Topology.Category.TopCat.Adjunctions` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.Topology.Maps.Proper.UniversallyClosed` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.Topology.Category.TopCat.Limits.Products` `Mathlib.Topology.Sets.Compacts` `Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves` `Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Topology.ContinuousFunction.T0Sierpinski` `Mathlib.CategoryTheory.Sites.DenseSubsite` `Mathlib.Topology.DiscreteQuotient` `Mathlib.Topology.UniformSpace.Pi` `Mathlib.Topology.Sets.Opens` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.Topology.Category.CompHausLike.Limits` `Mathlib.Algebra.Homology.Linear` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.CategoryTheory.Sites.Discrete` `Mathlib.Topology.KrullDimension` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Extensive` `Mathlib.Data.DFinsupp.Lex` `Mathlib.Topology.Sheaves.PUnit` `Mathlib.Topology.Compactness.Paracompact` `Mathlib.Topology.Sheaves.Presheaf` `Mathlib.CategoryTheory.Adhesive` `Mathlib.Topology.Category.TopCat.Limits.Basic` `Mathlib.Topology.IsLocalHomeomorph` `Mathlib.Topology.Algebra.Order.Rolle` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Topology.UniformSpace.UniformConvergenceTopology` `Mathlib.Topology.Category.UniformSpace` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.Topology.Category.FinTopCat` `Mathlib.Geometry.RingedSpace.PresheafedSpace` `Mathlib.Topology.UniformSpace.Equicontinuity` `Mathlib.Topology.Category.TopCat.EffectiveEpi` `Mathlib.Topology.Order.Hom.Basic` `Mathlib.Algebra.Module.LinearMap.Rat` `Mathlib.Topology.Algebra.Constructions.DomMulAct` `Mathlib.Data.DFinsupp.Order` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Topology.UniformSpace.Equiv` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent` `Mathlib.Algebra.Module.Rat` `Mathlib.Combinatorics.SimpleGraph.Ends.Properties` `Mathlib.CategoryTheory.Sites.Coherent.RegularTopology` `Mathlib.Topology.Category.TopCat.Limits.Pullbacks` `Mathlib.Topology.Support` `Mathlib.Topology.QuasiSeparated`	-4
3 files `Mathlib.Data.DFinsupp.WellFounded` `Mathlib.Combinatorics.Configuration` `Mathlib.Dynamics.BirkhoffSum.Average`	-2
2340 files `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Data.Real.Hyperreal` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Algebra.Star.Module` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.CategoryTheory.Abelian.Generator` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Combinatorics.Additive.ETransform` `Mathlib.LinearAlgebra.FinsuppVectorSpace` `Mathlib.Probability.Process.HittingTime` `Mathlib.LinearAlgebra.BilinearMap` `Mathlib.Algebra.Module.Zlattice.Covolume` `Mathlib.Data.Nat.Choose.Cast` `Mathlib.NumberTheory.Liouville.LiouvilleWith` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.Analysis.Calculus.Deriv.Pi` `Mathlib.RingTheory.Henselian` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Instances.Nat` `Mathlib.Algebra.Periodic` `Mathlib.Probability.BorelCantelli` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.NumberTheory.Wilson` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.Data.Real.Pointwise` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.RingTheory.PowerBasis` `Mathlib.Algebra.Symmetrized` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.IntermediateField` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.RingTheory.AlgebraTower` `Mathlib.Data.Matrix.Auto` `Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.ContinuousFunction.CompactlySupported` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.GroupTheory.Submonoid.Inverses` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.RingTheory.Ideal.QuotientOperations` `Mathlib.Probability.Variance` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.Topology.MetricSpace.Antilipschitz` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.GroupTheory.CoprodI` `Mathlib.Analysis.Complex.Angle` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.RingTheory.SimpleModule` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.LinearAlgebra.Finsupp` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.Analysis.Subadditive` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.Algebra.Module.LocalizedModuleIntegers` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.NumberTheory.Multiplicity` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.GroupTheory.Perm.Cycle.PossibleTypes` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.LinearAlgebra.Projection` `Mathlib.Algebra.Category.Grp.EpiMono` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Data.NNReal.Star` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.Calculus.Deriv.Star` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.LinearAlgebra.SModEq` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.LinearAlgebra.Span` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.RingTheory.Artinian` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Topology.Instances.PNat` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.FieldTheory.Laurent` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.LinearAlgebra.AffineSpace.Ordered` `Mathlib.NumberTheory.GaussSum` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Module.Submodule.Basic` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.Finsupp.Basic` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.Algebra.Order.Algebra` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Condensed.Limits` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.RingTheory.DedekindDomain.Ideal` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Topology.MetricSpace.ShrinkingLemma` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Flat.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Module.Algebra` `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Data.Real.GoldenRatio` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.Condensed.TopComparison` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Data.Finsupp.PWO` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Analysis.Hofer` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.Data.Matrix.Invertible` `Mathlib.Topology.Instances.Int` `Mathlib.Analysis.Convex.Topology` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Logic.Hydra` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Lie.Submodule` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.Data.Matrix.Composition` `Mathlib.RingTheory.ClassGroup` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Data.Set.Pointwise.Iterate` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.GroupTheory.DoubleCoset` `Mathlib.Probability.StrongLaw` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Algebra.Category.Grp.AB5` `Mathlib.Data.Real.ENatENNReal` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.Data.Matrix.Basic` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Data.ZMod.Module` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Data.Matrix.Basis` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.GroupTheory.Perm.Cycle.Basic` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.Complex.Isometry` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.GroupTheory.Coset` `Mathlib.Analysis.Convex.Side` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.LinearAlgebra.PID` `Mathlib.RingTheory.LaurentSeries` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.Analysis.Convex.Body` `Mathlib.Topology.Category.Profinite.Nobeling` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Condensed.Light.Explicit` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Module.Submodule.Map` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Probability.CondCount` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Data.Real.Sqrt` `Mathlib.Topology.ContinuousFunction.Ideals` `Mathlib.LinearAlgebra.QuadraticForm.Prod` `Mathlib.FieldTheory.Galois` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.RingTheory.Trace.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Data.Finsupp.Encodable` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.GroupTheory.OrderOfElement` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.NumberTheory.FLT.Four` `Mathlib.GroupTheory.GroupAction.ConjAct` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Algebra.RingQuot` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.Topology.Germ` `Mathlib.Data.ENNReal.Inv` `Mathlib.Topology.MetricSpace.Sequences` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.FieldTheory.Normal` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.GroupTheory.FreeAbelianGroupFinsupp` `Mathlib.Probability.Kernel.Composition` `Mathlib.NumberTheory.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Dynamics.OmegaLimit` `Mathlib.Data.Real.ConjExponents` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.LinearAlgebra.FreeModule.IdealQuotient` `Mathlib.GroupTheory.Perm.Closure` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.GroupTheory.Abelianization` `Mathlib.Data.Finset.SMulAntidiagonal` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.CategoryTheory.Preadditive.Generator` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.RingTheory.Jacobson` `Mathlib.GroupTheory.GroupExtension.Defs` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Algebra.Quaternion` `Mathlib.Condensed.Explicit` `Mathlib.NumberTheory.MulChar.Basic` `Mathlib.Data.Nat.Choose.Lucas` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Norm.Defs` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.GroupTheory.Exponent` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.Condensed.Module` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.FieldTheory.Adjoin` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.NumberTheory.NumberField.Discriminant` `Mathlib.GroupTheory.Solvable` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Topology.Sheaves.Forget` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Analysis.Oscillation` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.Topology.ContinuousFunction.ContinuousMapZero` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.Algebra.DualQuaternion` `Mathlib.RingTheory.Localization.Integral` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.Analysis.Complex.Circle` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Data.ZMod.Quotient` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.Algebra.Exact` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.NumberTheory.RamificationInertia` `Mathlib.Data.Nat.Squarefree` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Data.Nat.Factorization.Induction` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Topology.ContinuousFunction.Polynomial` `Mathlib.LinearAlgebra.TensorProduct.Prod` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.LinearAlgebra.QuadraticForm.Basic` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Module.Submodule.Range` `Mathlib.LinearAlgebra.QuadraticForm.Basis` `Mathlib.RepresentationTheory.Rep` `Mathlib.Combinatorics.Additive.AP.Three.Defs` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.LinearAlgebra.Matrix.Determinant.Misc` `Mathlib.Data.Finsupp.Weight` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.MeasureTheory.Function.LpSpace` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.CategoryTheory.Abelian.ProjectiveResolution` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.GroupTheory.Divisible` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.RingTheory.Ideal.MinimalPrime` `Mathlib.GroupTheory.Nilpotent` `Mathlib.Topology.MetricSpace.Cauchy` `Mathlib.GroupTheory.GroupAction.FixedPoints` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.GroupTheory.FreeGroup.NielsenSchreier` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.GroupTheory.CommutingProbability` `Mathlib.Algebra.Lie.Free` `Mathlib.RingTheory.TwoSidedIdeal.Lattice` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Analysis.Complex.Basic` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Topology.MetricSpace.Lipschitz` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.NoncommPiCoprod` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.Algebra.Order.ToIntervalMod` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.LinearAlgebra.PerfectPairing` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Data.Nat.Periodic` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Topology.Instances.Discrete` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.LinearAlgebra.QuotientPi` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.Noetherian` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.LinearAlgebra.Trace` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.CategoryTheory.Action` `Mathlib.Algebra.Polynomial.DenomsClearable` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Algebra.Algebra.Subalgebra.Rank` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Topology.Instances.AddCircle` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.Topology.ContinuousFunction.Algebra` `Mathlib.Analysis.Convex.Slope` `Mathlib.Data.Set.Pointwise.Support` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.RingTheory.Ideal.Quotient` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Algebra.Algebra.Basic` `Mathlib.FieldTheory.Fixed` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.GroupTheory.Perm.Fin` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Topology.Order.Bounded` `Mathlib.Data.Matrix.CharP` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Topology.Bornology.Absorbs` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Algebra.Algebra.Operations` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.Order.Filter.Pointwise` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.Data.ZMod.Coprime` `Mathlib.Algebra.Star.StarAlgHom` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Topology.CompletelyRegular` `Mathlib.Algebra.Lie.Basic` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Convex.Cone.Pointed` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Order.Monovary` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.Data.Complex.Exponential` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.GroupTheory.Perm.Cycle.Factors` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Homology.DerivedCategory.Ext` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.Geometry.Manifold.SmoothManifoldWithCorners` `Mathlib.Condensed.Basic` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.Algebra.Lie.Killing` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Topology.MetricSpace.Dilation` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.GroupTheory.GroupAction.Period` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.Algebra.Lie.Character` `Mathlib.Topology.ContinuousFunction.StarOrdered` `Mathlib.Algebra.Group.AddChar` `Mathlib.RingTheory.Presentation` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Probability.Martingale.Basic` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.Topology.MetricSpace.ProperSpace` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.LinearAlgebra.FiniteDimensional` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.Geometry.Manifold.InteriorBoundary` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.FieldTheory.Extension` `Mathlib.LinearAlgebra.Orientation` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Data.Matrix.Block` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.Normed.Ring.SeminormFromConst` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.Topology.UrysohnsBounded` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Data.ZMod.IntUnitsPower` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.Topology.Algebra.Star` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.Real` `Mathlib.RingTheory.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.RingTheory.Flat.Algebra` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.GroupTheory.Perm.DomMulAct` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.GroupTheory.GroupAction.Pointwise` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.NumberTheory.Rayleigh` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Combinatorics.Additive.RuzsaCovering` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Condensed.Solid` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Topology.List` `Mathlib.FieldTheory.KrullTopology` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Probability.Kernel.IntegralCompProd` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.Radical` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.RingTheory.Localization.Integer` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.Analysis.Normed.Ring.Seminorm` `Mathlib.Algebra.Order.Nonneg.Module` `Mathlib.RingTheory.Generators` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Data.Complex.Determinant` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.CategoryTheory.Limits.Shapes.SingleObj` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.Data.Finset.Finsupp` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.Analysis.PSeriesComplex` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.RingTheory.QuotientNilpotent` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.Topology.MetricSpace.IsometricSMul` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.LinearAlgebra.AffineSpace.MidpointZero` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Analysis.Convex.Integral` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.GroupTheory.QuotientGroup` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Algebra.LinearRecurrence` `Mathlib.MeasureTheory.Constructions.Prod.Integral` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.Algebra.AddTorsor` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian` `Mathlib.GroupTheory.FiniteAbelian` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.LinearAlgebra.AffineSpace.Basic` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.LinearAlgebra.CliffordAlgebra.Star` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Topology.MetricSpace.Isometry` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Algebra.Algebra.Pi` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.Condensed.Light.Epi` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.RingTheory.ZMod` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.LinearAlgebra.Matrix.Nondegenerate` `Mathlib.Data.Matrix.Reflection` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Algebra.Module.Projective` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Data.DFinsupp.Interval` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.CategoryTheory.Abelian.Injective` `Mathlib.Dynamics.Newton` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Convex.Join` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.FieldTheory.MvPolynomial` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RepresentationTheory.Character` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Module` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.NumberTheory.SmoothNumbers` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.RingTheory.TwoSidedIdeal.Basic` `Mathlib.Topology.TietzeExtension` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.LinearAlgebra.CliffordAlgebra.Equivs` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.Algebra.Order.Chebyshev` `Mathlib.RepresentationTheory.Basic` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.NumberTheory.FLT.Three` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.RingTheory.Filtration` `Mathlib.Testing.SlimCheck.Functions` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.SpecialFunctions.Polynomials` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.GroupTheory.CosetCover` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.Topology.MetricSpace.Infsep` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.CategoryTheory.Abelian.Projective` `Mathlib.LinearAlgebra.CliffordAlgebra.Fold` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.LinearAlgebra.FreeModule.Finite.Matrix` `Mathlib.LinearAlgebra.Matrix.Charpoly.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.Topology.Instances.Rat` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.RingTheory.Algebraic` `Mathlib.Topology.Algebra.ProperAction` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Probability.Kernel.Invariance` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.Tactic.ComputeDegree` `Mathlib.Probability.Distributions.Uniform` `Mathlib.SetTheory.Surreal.Dyadic` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Algebra.Lie.Matrix` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.Data.Matrix.Rank` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.Liouville.Measure` `Mathlib.LinearAlgebra.Pi` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.GroupTheory.Torsion` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Topology.ContinuousFunction.Weierstrass` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.LinearAlgebra.LinearIndependent` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.Analysis.Convex.Between` `Mathlib.GroupTheory.FixedPointFree` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Topology.Compactness.PseudometrizableLindelof` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.NumberTheory.Ostrowski` `Mathlib.GroupTheory.GroupAction.Support` `Mathlib.Data.Real.Irrational` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.Algebra.Polynomial.Induction` `Mathlib.LinearAlgebra.Contraction` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.Algebra.Algebra.Spectrum` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Analysis.MeanInequalities` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.Algebra.Star.CHSH` `Mathlib.Probability.Distributions.Poisson` `Mathlib.RingTheory.Binomial` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Algebra.Module.Submodule.RestrictScalars` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.Polynomial.Chebyshev` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.Analysis.Normed.Ring.SeminormFromBounded` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.Even` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.LinearAlgebra.Multilinear.FiniteDimensional` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Algebra.Module.Submodule.Localization` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.Algebra.Module.Zlattice.Basic` `Mathlib.Analysis.InnerProductSpace.Projection` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Computability.TMComputable` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Data.ZMod.Basic` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.RingTheory.MvPolynomial.Symmetric` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Analysis.Convex.Independent` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.Analysis.Calculus.Deriv.Prod` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Probability.ConditionalProbability` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Order.Filter.ENNReal` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Topology.Algebra.Field` `Mathlib.Logic.Equiv.TransferInstance` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Topology.ContinuousFunction.Units` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.RingTheory.OrzechProperty` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.GroupTheory.Perm.Cycle.Concrete` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.Analysis.Quaternion` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Algebra.Lie.Abelian` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Matrix.Kronecker` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.RingTheory.HopfAlgebra` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Data.ZMod.Parity` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.GroupTheory.Commensurable` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Algebra.Star.RingQuot` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.RingTheory.Discriminant` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.GroupTheory.Complement` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Algebra.Order.Pointwise` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.Algebra.Group.Submonoid.Units` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.DirectLimit` `Mathlib.MeasureTheory.Measure.VectorMeasure` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.Analysis.Analytic.Meromorphic` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.Algebra.Module.PID` `Mathlib.RepresentationTheory.Action.Monoidal` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.LinearAlgebra.CliffordAlgebra.Inversion` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.FieldTheory.Finiteness` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.UnitInterval` `Mathlib.Topology.UrysohnsLemma` `Mathlib.RepresentationTheory.Action.Limits` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Algebra.Pointwise.Stabilizer` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.Analysis.Complex.Tietze` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Data.Real.StarOrdered` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.Algebra.CharP.ExpChar` `Mathlib.Topology.Metrizable.Basic` `Mathlib.MeasureTheory.Function.L1Space` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.RingTheory.JacobsonIdeal` `Mathlib.Data.Finset.NatDivisors` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Analysis.Convex.Normed` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Probability.Kernel.Basic` `Mathlib.GroupTheory.Index` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Complex.Liouville` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.GroupTheory.Perm.Finite` `Mathlib.Topology.Algebra.UniformGroup` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.Data.Finset.Pointwise.Card` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.MeasureTheory.Constructions.Prod.Basic` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.LinearAlgebra.Ray` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.Algebra.Module.Submodule.IterateMapComap` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.CategoryTheory.Triangulated.Opposite` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Algebra.Homology.ComplexShapeSigns` `Mathlib.Analysis.Convex.Segment` `Mathlib.Data.ZMod.Units` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.FieldTheory.Perfect` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.Algebra.Module.Injective` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Data.Complex.Cardinality` `Mathlib.Algebra.Homology.Localization` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.RingTheory.UniqueFactorizationDomain` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.Analysis.Convex.Measure` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.Probability.Moments` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Algebra.Group.Submonoid.Pointwise` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.Algebra.Order.UpperLower` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.FieldTheory.Cardinality` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Topology.Algebra.Group.TopologicalAbelianization` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.RCLike.Basic` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Topology.Algebra.Algebra` `Mathlib.NumberTheory.Dioph` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Algebra.Module.Torsion` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.Analysis.Complex.Conformal` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.Instances.Complex` `Mathlib.MeasureTheory.MeasurableSpace.Basic` `Mathlib.Logic.Small.Group` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.NumberTheory.Liouville.Basic` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.Grading` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Data.Nat.Factorization.Root` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.Data.ZMod.Factorial` `Mathlib.Algebra.Module.Submodule.Lattice` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.GroupTheory.Perm.ClosureSwap` `Mathlib.FieldTheory.Separable` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Algebra.Module.Submodule.Equiv` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Analysis.Normed.Operator.WeakOperatorTopology` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Algebra.Algebra.Quasispectrum` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.Algebra.Star.Free` `Mathlib.Data.Finset.Pointwise.Basic` `Mathlib.RingTheory.Int.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.Analysis.NormedSpace.ENorm` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Topology.Algebra.Affine` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.Logic.Small.Module` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra` `Mathlib.RingTheory.Localization.Basic` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.LinearAlgebra.CliffordAlgebra.Basic` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.Algebra.Order.Module.OrderedSMul` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise` `Mathlib.Topology.ContinuousFunction.LocallyConstant` `Mathlib.RingTheory.AlgebraicIndependent` `Mathlib.LinearAlgebra.Vandermonde` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.Topology.Category.Compactum` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Dynamics.Minimal` `Mathlib.NumberTheory.Pell` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Probability.Process.Stopping` `Mathlib.Algebra.Category.AlgebraCat.Monoidal` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.NumberTheory.Modular` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.Tactic.ReduceModChar` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.Algebra.Polynomial.Eval` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.GroupTheory.Transfer` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Data.Multiset.Interval` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.RepresentationTheory.FDRep` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.GroupTheory.GroupAction.Blocks` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.Topology.ContinuousFunction.Compact` `Mathlib.GroupTheory.Finiteness` `Mathlib.Analysis.Analytic.Composition` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.MetricSpace.Basic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.CategoryTheory.Preadditive.ProjectiveResolution` `Mathlib.Topology.Sheaves.PresheafOfFunctions` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.GroupTheory.GroupAction.Basic` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.RingTheory.Bezout` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.SetTheory.Surreal.Multiplication` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv` `Mathlib.FieldTheory.NormalClosure` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Geometry.Manifold.IntegralCurve` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.GroupTheory.PresentedGroup` `Mathlib.Topology.Instances.EReal` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.LinearAlgebra.Reflection` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Data.Complex.Order` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Algebra.Prod` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Data.ENNReal.Real` `Mathlib.NumberTheory.FermatPsp` `Mathlib.Combinatorics.SetFamily.CauchyDavenport` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.GroupTheory.Sylow` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Probability.Kernel.MeasureCompProd` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Combinatorics.SimpleGraph.DegreeSum` `Mathlib.Analysis.Convex.Deriv` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.RingTheory.LocalProperties` `Mathlib.Topology.MetricSpace.Gluing` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.Probability.Independence.Basic` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.Algebra.Module.Submodule.EqLocus` `Mathlib.Algebra.Order.Module.Pointwise` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.RingTheory.MatrixAlgebra` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.Algebra.Category.AlgebraCat.Basic` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.Topology.ContinuousFunction.ZeroAtInfty` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.Convex.Uniform` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.RepresentationTheory.Action.Continuous` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.Idempotents` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Dynamics.Flow` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Probability.IdentDistrib` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.RingTheory.Complex` `Mathlib.Analysis.Convolution` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.LinearAlgebra.Matrix.Adjugate` `Mathlib.Data.Complex.Module` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Data.ENNReal.Operations` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.FieldTheory.KummerExtension` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Condensed.Light.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.GroupTheory.GroupAction.Quotient` `Mathlib.LinearAlgebra.QuadraticForm.Isometry` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.Topology.Instances.Irrational` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Analysis.MellinInversion` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.RingTheory.RingHomProperties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Topology.Sheaves.Operations` `Mathlib.Data.Real.EReal` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.Condensed.Light.Module` `Mathlib.Data.Real.Cardinality` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.Topology.Category.Sequential` `Mathlib.GroupTheory.PushoutI` `Mathlib.Analysis.Convex.Strict` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Data.Finset.Pointwise.Interval` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian` `Mathlib.Algebra.CharP.Reduced` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.CharZero.Quotient` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.Analysis.Complex.Convex` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.Category.Locale` `Mathlib.NumberTheory.PrimeCounting` `Mathlib.LinearAlgebra.Dual` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.Algebra.Group.Subgroup.Pointwise` `Mathlib.Topology.MetricSpace.ProperSpace.Lemmas` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv` `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.ModelTheory.Fraisse` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.RingTheory.Finiteness` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.GroupTheory.HNNExtension` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.GroupTheory.SpecificGroups.Alternating` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.Analysis.Convex.Hull` `Mathlib.RingTheory.Fintype` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.RingTheory.Etale.Basic` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Analysis.Convex.Star` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Topology.Algebra.Order.Group` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.Data.ZMod.Algebra` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.Algebra.Order.CompleteField` `Mathlib.RingTheory.Ideal.Norm` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.Data.Finsupp.Lex` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.NumberTheory.WellApproximable` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Convex.Basic` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.LinearAlgebra.CliffordAlgebra.Contraction` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Algebra.Module.PointwisePi` `Mathlib.Topology.MetricSpace.Bilipschitz` `Mathlib.CategoryTheory.Abelian.InjectiveResolution` `Mathlib.InformationTheory.Hamming` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Algebra.CharP.Algebra` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.RingTheory.Localization.Module` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Probability.Process.Adapted` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Topology.ContinuousFunction.Bounded` `Mathlib.Data.Finsupp.Interval` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.Algebra.Lie.Sl2` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.Data.Nat.Factorial.Cast` `Mathlib.Analysis.Convex.Complex` `Mathlib.Data.Matrix.RowCol` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.FieldTheory.PurelyInseparable` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Algebra.Group.UniqueProds` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.CategoryTheory.Preadditive.InjectiveResolution` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.Analysis.Analytic.Within` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Probability.Independence.Kernel` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.Order.Category.Frm` `Mathlib.Topology.Algebra.Localization` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.NumberTheory.NumberField.House` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.Algebra.Lie.Solvable` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.Condensed.Epi` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.Probability.Process.Filtration` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.LinearAlgebra.TensorPower` `Mathlib.RingTheory.MvPolynomial.NewtonIdentities` `Mathlib.Algebra.QuaternionBasis` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.Bernoulli` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.Analysis.MellinTransform` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Data.Matrix.Hadamard` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.ModelTheory.DirectLimit` `Mathlib.Algebra.Lie.Engel` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Data.Set.Pointwise.SMul` `Mathlib.Analysis.Normed.Field.InfiniteSum` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Algebra.Lie.Rank` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Data.Set.Pointwise.Finite` `Mathlib.Condensed.Light.Functors` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.GroupTheory.Order.Min` `Mathlib.Analysis.Asymptotics.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.LinearAlgebra.CliffordAlgebra.Prod` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.CharP.Two` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.Data.Complex.Abs` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.NumberTheory.Liouville.Residual` `Mathlib.Topology.Algebra.Order.Floor` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.RingTheory.MaximalSpectrum` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.RingTheory.Unramified.Derivations` `Mathlib.Probability.Distributions.Gamma` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.RingTheory.Flat.Stability` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.RingTheory.FiniteType` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.Condensed.Functors` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.MeasureTheory.Group.Action` `Mathlib.Probability.Density` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Data.Nat.Factorization.PrimePow` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Data.Finsupp.AList` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC` `Mathlib.GroupTheory.GroupAction.FixingSubgroup` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.Condensed.Equivalence` `Mathlib.Data.Complex.Orientation` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Calculus.Dslope` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Data.ENNReal.Basic` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.RingTheory.IntegralDomain` `Mathlib.Algebra.Algebra.Hom` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.GroupTheory.SpecificGroups.Dihedral` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.Topology.Instances.NNReal` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.FieldTheory.Tower` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Algebra.Module.Submodule.Order` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.RingTheory.PrimeSpectrum` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.GroupTheory.Frattini` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Data.Finsupp.Order` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.Algebra.CharP.CharAndCard` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.GroupTheory.PGroup` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.GroupTheory.GroupAction.SubMulAction` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.RingTheory.FreeRing` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.Algebra.Algebra.NonUnitalHom` `Mathlib.Tactic` `Mathlib.Algebra.DualNumber` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.Algebra.Module.LocalizedModule` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Algebra.Star.Unitary` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.LinearAlgebra.FiniteSpan` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.Topology.ContinuousFunction.StoneWeierstrass` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Analysis.Convex.Radon` `Mathlib.LinearAlgebra.Matrix.IsDiag` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.LinearAlgebra.Prod` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.Topology.MetricSpace.DilationEquiv` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.Topology.Semicontinuous` `Mathlib.RingTheory.Support` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.RepresentationTheory.Maschke` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Probability.Integration` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.GroupTheory.Perm.Cycle.Type` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.NumberTheory.Bertrand` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.GroupTheory.Schreier` `Mathlib.RingTheory.NormTrace` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Data.Matrix.Notation` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.Algebra.Module.Submodule.LinearMap` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.Algebra.Algebra.Tower` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Algebra.Ring.NegOnePow` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Polynomial.Cardinal` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.RingTheory.QuotientNoetherian` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Combinatorics.SimpleGraph.Matching` `Mathlib.Algebra.Module.Submodule.Ker` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.Topology.Sheaves.Stalks` `Mathlib.Probability.Independence.Conditional` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.Algebra.ModEq` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.RingTheory.Perfection` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.RingTheory.Norm.Basic` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Notation` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.FunctionField` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Probability.CDF` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.NumberTheory.DiophantineApproximation` `Mathlib.Data.Nat.Totient` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.Analysis.Convex.Exposed` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Topology.Instances.ENNReal` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.Probability.Martingale.Centering` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.GroupTheory.FreeAbelianGroup` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.Topology.Instances.RatLemmas` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Topology.MetricSpace.Bounded` `Mathlib.Logic.Small.Ring` `Mathlib.LinearAlgebra.Matrix.Block` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.Geometry.Manifold.ContMDiff.Product` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.LinearAlgebra.Quotient` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Topology.Algebra.ContinuousMonoidHom` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Data.Nat.Factorial.SuperFactorial`	-1
8 files `Mathlib.GroupTheory.Coprod.Basic` `Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero` `Mathlib.Algebra.Tropical.Lattice` `Mathlib.Algebra.Tropical.Basic` `Mathlib.Algebra.Tropical.BigOperators` `Mathlib.GroupTheory.MonoidLocalization.Order` `Mathlib.GroupTheory.MonoidLocalization.Basic` `Mathlib.Algebra.Group.Subgroup.Actions`	1
6 files `Mathlib.RingTheory.Congruence.BigOperators` `Mathlib.RingTheory.OreLocalization.Basic` `Mathlib.RingTheory.Congruence.Opposite` `Mathlib.Algebra.Ring.Action.Subobjects` `Mathlib.RingTheory.Congruence.Basic` `Mathlib.Algebra.SMulWithZero`	2
`Mathlib.Algebra.GroupWithZero.Action.Opposite`	3
3 files `Mathlib.GroupTheory.GroupAction.DomAct.Basic` `Mathlib.GroupTheory.GroupAction.BigOperators` `Mathlib.GroupTheory.Congruence.BigOperators`	5
4 files `Mathlib.GroupTheory.Congruence.Opposite` `Mathlib.Algebra.GroupWithZero.Action.Prod` `Mathlib.GroupTheory.Congruence.Basic` `Mathlib.Algebra.Group.Submonoid.DistribMulAction`	6
`Mathlib.Algebra.GroupWithZero.Action.Units`	7
`Mathlib.Algebra.Ring.Action.Basic`	8
`Mathlib.Algebra.GroupWithZero.Action.Pi`	14
`Mathlib.Algebra.GroupWithZero.Action.Defs`	23

Declarations diff

+ IsUnit.smul_eq_zero
- smul_eq_zero

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.

Ruben-VandeVelde

maintainer merge

github-actions · 2024-08-15T21:42:45Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

jcommelin · 2024-08-16T12:58:24Z

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

+import Mathlib.Algebra.Group.Action.Units
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Algebra.GroupWithZero.Units.Basic


This seems to amount to a 12% increase of the number transitive imports...

Since this is a Defs file, I would rather prefer to see the number go down.

It is a very recent Defs file, however. I am still working on it. Here are my future plans:

Move some of the content from GroupTheory.GroupAction.Group to this file (this PR)

Move most of the content of Algebra.SMulWithZero to this file (not yet opened, but you can see the result in chore: Move group actions #13027)

Think about a nice way to split things into Defs and Basic

I can't really do the last step before the first two, so I would rather stick to my plan and declare this temporary 12% increase as fine.

Why can't you do (2) first and then (1) and (3) simultaneously, without the large-ish increase in transitive imports?

(2) will increase imports as well. Furthermore, (1) + (3) together would be a multiway split, not very reviewer-friendly

j-loreaux · 2024-08-16T18:41:35Z

@jcommelin I'll let you decide, since you initially raised the objection. I'm content with Yaël's indication to later split the file into Defs + Basic in some helpful way.

jcommelin · 2024-08-19T07:50:47Z

Ok, let's go ahead.

bors merge

All lemmas can be moved to earlier files

mathlib-bors · 2024-08-19T09:50:20Z

Pull request successfully merged into master.

Build succeeded:

All lemmas can be moved to earlier files

chore(GroupTheory/GroupAction/Group): Delete

464d5a2

All lemmas can be moved to earlier files

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels Aug 14, 2024

YaelDillies mentioned this pull request Aug 14, 2024

chore: Move group actions #13027

Open

19 tasks

YaelDillies added 2 commits August 14, 2024 15:18

fix

efa2d02

fix Algebra.Order.Module.OrderedSMul

3b3f0ba

Ruben-VandeVelde approved these changes Aug 15, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Aug 15, 2024

jcommelin reviewed Aug 16, 2024

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 16, 2024

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 16, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 19, 2024

mathlib-bors bot pushed a commit that referenced this pull request Aug 19, 2024

chore(GroupTheory/GroupAction/Group): Delete (#15806)

8333413

All lemmas can be moved to earlier files

mathlib-bors bot changed the title ~~chore(GroupTheory/GroupAction/Group): Delete~~ [Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete Aug 19, 2024

mathlib-bors bot closed this Aug 19, 2024

mathlib-bors bot deleted the delete_group_action_group branch August 19, 2024 09:50

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore(GroupTheory/GroupAction/Group): Delete (#15806)

76a5393

All lemmas can be moved to earlier files

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024

chore(GroupTheory/GroupAction/Group): Delete (#15806)

fde5097

All lemmas can be moved to earlier files

bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024

chore(GroupTheory/GroupAction/Group): Delete (#15806)

eee1c6b

All lemmas can be moved to earlier files

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete #15806

[Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete #15806

YaelDillies commented Aug 14, 2024

github-actions bot commented Aug 14, 2024 •

edited

Loading

Import changes for modified files

Ruben-VandeVelde left a comment

github-actions bot commented Aug 15, 2024

jcommelin Aug 16, 2024

YaelDillies Aug 16, 2024

j-loreaux Aug 16, 2024 •

edited

Loading

YaelDillies Aug 16, 2024 •

edited

Loading

j-loreaux commented Aug 16, 2024

jcommelin commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

[Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete #15806

[Merged by Bors] - chore(GroupTheory/GroupAction/Group): Delete #15806

Conversation

YaelDillies commented Aug 14, 2024

github-actions bot commented Aug 14, 2024 • edited Loading

PR summary 3b3f0ba668

Import changes for modified files

Declarations diff

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

github-actions bot commented Aug 15, 2024

jcommelin Aug 16, 2024

Choose a reason for hiding this comment

YaelDillies Aug 16, 2024

Choose a reason for hiding this comment

j-loreaux Aug 16, 2024 • edited Loading

Choose a reason for hiding this comment

YaelDillies Aug 16, 2024 • edited Loading

Choose a reason for hiding this comment

j-loreaux commented Aug 16, 2024

jcommelin commented Aug 19, 2024

mathlib-bors bot commented Aug 19, 2024

github-actions bot commented Aug 14, 2024 •

edited

Loading

j-loreaux Aug 16, 2024 •

edited

Loading

YaelDillies Aug 16, 2024 •

edited

Loading