feat: add IsMulCommutative instances for directed families of commutative subobjects#36553
Open
j-loreaux wants to merge 12 commits intoleanprover-community:masterfrom
Open
feat: add IsMulCommutative instances for directed families of commutative subobjects#36553j-loreaux wants to merge 12 commits intoleanprover-community:masterfrom
j-loreaux wants to merge 12 commits intoleanprover-community:masterfrom
Conversation
PR summary d194281a48
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Star.Subalgebra | 1030 | 1031 | +1 (+0.10%) |
Import changes for all files
| Files | Import difference |
|---|---|
886 filesMathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.Algebra.Star.Subalgebra Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.WithLp Mathlib.Analysis.Asymptotics.ExpGrowth Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.Unitary.Maps Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.ContDiff.Convolution Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.Deriv.MeanValue Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.DerivativeTest Mathlib.Analysis.Calculus.DifferentialForm.Basic Mathlib.Analysis.Calculus.DifferentialForm.VectorField Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.ImplicitContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.CanonicalDecomposition Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.CoveringMap Mathlib.Analysis.Complex.ExponentialBounds Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.Liouville Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.Harmonic.Poisson Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Poisson Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.Spectrum Mathlib.Analysis.Complex.SqrtDeriv Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.Approximation Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.TensorProduct Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.DerivNotation Mathlib.Analysis.Distribution.Distribution Mathlib.Analysis.Distribution.FourierMultiplier Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace.Basic Mathlib.Analysis.Distribution.SchwartzSpace.Deriv Mathlib.Analysis.Distribution.SchwartzSpace.Fourier Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Distribution.Support Mathlib.Analysis.Distribution.TemperateGrowth Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Distribution.TestFunction Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar Mathlib.Analysis.Fourier.Convolution Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.LpSpace Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Affine Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.CanonicalTensor Mathlib.Analysis.InnerProductSpace.Coalgebra Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramMatrix Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.Harmonic.Analytic Mathlib.Analysis.InnerProductSpace.Harmonic.Basic Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl Mathlib.Analysis.InnerProductSpace.Laplacian Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.MulOpposite Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection.Basic Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional Mathlib.Analysis.InnerProductSpace.Projection.Minimal Mathlib.Analysis.InnerProductSpace.Projection.Reflection Mathlib.Analysis.InnerProductSpace.Projection.Submodule Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TensorProduct Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.Montel Mathlib.Analysis.LocallyConvex.SeparatingDual Mathlib.Analysis.LocallyConvex.Separation Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix.Hermitian Mathlib.Analysis.Matrix.Normed Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Meromorphic.FactorizedRational Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Algebra.DualNumber Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Field.Approximation Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.Matrix Mathlib.Analysis.Normed.Lp.MeasurableSpace Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.SmoothApprox Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.DoubleDual Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Module.Normalize Mathlib.Analysis.Normed.Module.RCLike.Basic Mathlib.Analysis.Normed.Module.RCLike.Extend Mathlib.Analysis.Normed.Module.RieszLemma Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.CompleteCodomain Mathlib.Analysis.Normed.Operator.FredholmAlternative Mathlib.Analysis.Normed.Ring.InfiniteProd Mathlib.Analysis.Normed.Unbundled.AlgebraNorm Mathlib.Analysis.Normed.Unbundled.FiniteExtension Mathlib.Analysis.Normed.Unbundled.InvariantExtension Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful Mathlib.Analysis.Normed.Unbundled.RingSeminorm Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded Mathlib.Analysis.Normed.Unbundled.SeminormFromConst Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.Polynomial.Fourier Mathlib.Analysis.Polynomial.Norm Mathlib.Analysis.Polynomial.Order Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.RCLike.BoundedContinuous Mathlib.Analysis.RCLike.Extend Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.RCLike.Sqrt Mathlib.Analysis.RCLike.TangentCone Mathlib.Analysis.Real.Pi.Bounds Mathlib.Analysis.Real.Pi.Chudnovsky Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Arcosh Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.Artanh Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.CircleMap Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gamma.Digamma Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrability.Basic Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic Mathlib.Analysis.SpecialFunctions.Integrals.Basic Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.InvLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.Pochhammer Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.Sigmoid Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Computability.AkraBazzi.SumTransform Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Dynamics.TopologicalEntropy.Subset Mathlib.Geometry.Diffeology.Basic Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Incenter Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.NinePointCircle Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity Mathlib.Geometry.Euclidean.Simplex Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.OrthRadius Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Sphere.Tangent Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Euclidean.Volume.Measure Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Constructions Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.GroupLieAlgebra Mathlib.Geometry.Manifold.Immersion Mathlib.Geometry.Manifold.Instances.Icc Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.IsManifold.ExtChartAt Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.LocalSourceTargetProperty Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.Notation Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.Riemannian.PathELength Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.SmoothApprox Mathlib.Geometry.Manifold.SmoothEmbedding Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.LocalFrame Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.Riemannian Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorBundle.Tensoriality Mathlib.Geometry.Manifold.VectorField.LieBracket Mathlib.Geometry.Manifold.VectorField.Pullback Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.ChainRule Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Stochastic Mathlib.LinearAlgebra.Matrix.Swap Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AbsolutelyContinuous Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ConditionalLExpectation Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.ConvergenceInDistribution Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.MeasureTheory.Function.Holder Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.JacobianOneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.Count Mathlib.MeasureTheory.Function.LpSeminorm.Defs Mathlib.MeasureTheory.Function.LpSeminorm.Indicator Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity Mathlib.MeasureTheory.Function.LpSeminorm.Prod Mathlib.MeasureTheory.Function.LpSeminorm.SMul Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.MeasureTheory.Function.LpSpace.Basic Mathlib.MeasureTheory.Function.LpSpace.Complete Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace.Indicator Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.Basic Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus Mathlib.MeasureTheory.Integral.Bochner.L1 Mathlib.MeasureTheory.Integral.Bochner.Set Mathlib.MeasureTheory.Integral.Bochner.SumMeasure Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleAverage Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.CompactlySupported Mathlib.MeasureTheory.Integral.CurveIntegral.Basic Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FinMeasAdditive Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.MeanValue Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Regular Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion Mathlib.MeasureTheory.Measure.CharacteristicFunction Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureExt Mathlib.MeasureTheory.Measure.FiniteMeasurePi Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.DistribChar Mathlib.MeasureTheory.Measure.Haar.Extension Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.IntegralCharFun Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyConvergence Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.Prokhorov Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.TightNormed Mathlib.MeasureTheory.Measure.Tight Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap Mathlib.MeasureTheory.SpecificCodomains.Pi Mathlib.MeasureTheory.SpecificCodomains.WithLp Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.Chebyshev Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.Basic Mathlib.NumberTheory.Height.MvPolynomial Mathlib.NumberTheory.Height.Projectivization Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp Mathlib.NumberTheory.ModularForms.Cusps Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Modular Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Niven Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.ZetaValues Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.Distributions.TwoValued Mathlib.Probability.Distributions.Uniform Mathlib.Probability.HasLawExists Mathlib.Probability.HasLaw Mathlib.Probability.IdentDistribIndep Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.BoundedContinuousFunction Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.Integration Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.RadonNikodym Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.Representation Mathlib.Probability.Kernel.SetIntegral Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.CovarianceBilinDual Mathlib.Probability.Moments.Covariance Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.Kolmogorov Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.RingTheory.HahnSeries.HahnEmbedding Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.BDeRham Mathlib.RingTheory.Perfectoid.FontaineTheta Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.PowerSeries.Restricted Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.Teichmuller Mathlib.RingTheory.Valuation.DiscreteValuativeRel Mathlib.RingTheory.Valuation.RankOne Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized Mathlib.Tactic.NormNum.Irrational Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactification.OnePoint.Sphere Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.ContinuousSqrt Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.EMetricSpace.PairReduction Mathlib.Topology.Instances.Complex Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.Snowflaking Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.MetricSpace.UniformConvergence Mathlib.Topology.VectorBundle.Riemannian |
1 |
Declarations diff
+ coe_iSup_of_directed
+++++++++++ instIsMulCommutative_iSup
+++++++++++ isMulCommutative_iSup
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
3 tasks
j-loreaux
added
blocked-by-other-PR
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
github-actions
bot
removed
the
merge-conflict
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
IsMulCommutativeubiquitously for subobjects #36549