feat(Data/Sym/Sym2): fromRel equivalence with Sigma over a Quotient

[SnirBroshi]

Add a non-dependent recursor on members of a fromRel set, and the following Equivs:

• The fromRel set of a symmetric relation r is equivalent to summing that set restricted to fibers of f.

• For a relation homomorphism r →r r' where r is symmetric, the fromRel set of r is equivalent to summing that set restricted to equivalence classes of r' using a Subtype.

---

I find this recursor pretty useful when dealing with fromRel, the idea came from a suggestion by @kmill on Zulip for another Sym2 conundrum.

[github-actions]

PR summary 5458d20504

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Sym.Sym2	475	477	+2 (+0.42%)

Import changes for all files

Files

Import difference

1524 files Mathlib.Algebra.BigOperators.Sym Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.ModuleCat.Descent Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.LinearMaps Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.DedekindDomain Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Module.Torsion.Basic Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.Algebra.Module.ZMod Mathlib.Algebra.MvPolynomial.NoZeroDivisors Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Algebra.QuadraticAlgebra.NormDeterminant Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.WithLp 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.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range 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.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span 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.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.Convolution Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.DifferentialForm.Basic Mathlib.Analysis.Calculus.DifferentialForm.VectorField Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.ImplicitContDiff Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.BorelCaratheodory Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.CoveringMap Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.DerivNotation 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.TemperateGrowth Mathlib.Analysis.Distribution.TemperedDistribution Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle 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.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.CanonicalTensor Mathlib.Analysis.InnerProductSpace.Coalgebra 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.JointEigenspace Mathlib.Analysis.InnerProductSpace.Laplacian Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.MulOpposite Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection.Basic Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional Mathlib.Analysis.InnerProductSpace.Projection.Reflection Mathlib.Analysis.InnerProductSpace.Projection.Submodule Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.TensorProduct Mathlib.Analysis.InnerProductSpace.Trace Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.Montel Mathlib.Analysis.LocallyConvex.SeparatingDual Mathlib.Analysis.LocallyConvex.Separation Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.Hermitian Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.Normed Mathlib.Analysis.Matrix.Order Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.Analysis.Matrix Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Meromorphic.Complex Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.Normed.Algebra.GelfandMazur Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Field.WithAbs Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.Matrix Mathlib.Analysis.Normed.Lp.MeasurableSpace Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.SmoothApprox Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Operator.CompleteCodomain Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.Real.Pi.Chudnovsky Mathlib.Analysis.Real.Pi.Irrational Mathlib.Analysis.Real.Pi.Leibniz Mathlib.Analysis.Real.Pi.Wallis Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass 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.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Configuration Mathlib.Combinatorics.Digraph.Orientation Mathlib.Combinatorics.Enumerative.Bell Mathlib.Combinatorics.Enumerative.Partition.Basic Mathlib.Combinatorics.Enumerative.Partition.GenFun Mathlib.Combinatorics.Enumerative.Partition.Glaisher Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.Graph.Basic Mathlib.Combinatorics.Nullstellensatz Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.DeleteEdges Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Extremal.Basic Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity Mathlib.Combinatorics.SimpleGraph.Extremal.Turan Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Hall Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.LineGraph Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Paths Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Combinatorics.SimpleGraph.VertexCover Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Combinatorics.SimpleGraph.Walks.Basic Mathlib.Combinatorics.SimpleGraph.Walks.Maps Mathlib.Combinatorics.SimpleGraph.Walks.Operations Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks Mathlib.Combinatorics.SimpleGraph.Walks.Traversal Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.Finset.Sym Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.WellFounded Mathlib.Data.List.Sym Mathlib.Data.Matrix.Cartan Mathlib.Data.Multiset.Sym Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.PowModTotient Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Data.Sym.Card Mathlib.Data.Sym.Sym2.Finsupp Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircleAdd Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.Ergodic.Extreme Mathlib.Dynamics.Ergodic.RadonNikodym Mathlib.FieldTheory.AbelRuffini Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.AlgebraicClosure Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.Cardinality Mathlib.FieldTheory.ChevalleyWarning Mathlib.FieldTheory.Differential.Basic Mathlib.FieldTheory.Differential.Liouville Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Finite.Basic Mathlib.FieldTheory.Finite.Extension Mathlib.FieldTheory.Finite.GaloisField Mathlib.FieldTheory.Finite.Polynomial Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.Galois.Abelian Mathlib.FieldTheory.Galois.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Galois.NormalBasis Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.IsSepClosed Mathlib.FieldTheory.Isaacs Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.KrullTopology Mathlib.FieldTheory.KummerExtension Mathlib.FieldTheory.KummerPolynomial Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.Minpoly.ConjRootClass Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.Normal.Basic Mathlib.FieldTheory.Normal.Closure Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.NormalizedTrace Mathlib.FieldTheory.PerfectClosure Mathlib.FieldTheory.Perfect Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.FieldTheory.PrimitiveElement Mathlib.FieldTheory.PurelyInseparable.Basic Mathlib.FieldTheory.PurelyInseparable.Exponent Mathlib.FieldTheory.PurelyInseparable.PerfectClosure Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Basic Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SeparablyGenerated Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Geometry.Diffeology.Basic Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector 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.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.NinePointCircle Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Similarity 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.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.ExtChartAt Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph 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.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.VectorField.LieBracket Mathlib.Geometry.Manifold.VectorField.Pullback Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.GroupAction.Jordan Mathlib.GroupTheory.GroupAction.MultiplePrimitivity Mathlib.GroupTheory.GroupAction.MultipleTransitivity Mathlib.GroupTheory.GroupAction.SubMulAction.Combination Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Perm.MaximalSubgroups Mathlib.GroupTheory.RegularWreathProduct Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Torsion Mathlib.GroupTheory.Transfer Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Center Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Complex.Determinant Mathlib.LinearAlgebra.Complex.Orientation Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.LinearAlgebra.Dual.BaseChange Mathlib.LinearAlgebra.Eigenspace.Charpoly Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.LinearAlgebra.ExteriorPower.Pairing Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient Mathlib.LinearAlgebra.FreeModule.ModN Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.Lagrange Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.Matrix.Charpoly.Disc Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Kronecker Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Rank Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.Stochastic Mathlib.LinearAlgebra.Matrix.Swap Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Vec Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Matrix Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.RootSystem.BaseChange Mathlib.LinearAlgebra.RootSystem.BaseExists Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Chain Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.G2 Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.Irreducible Mathlib.LinearAlgebra.RootSystem.IsValuedIn Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.LinearAlgebra.Semisimple Mathlib.LinearAlgebra.SesquilinearForm.Star Mathlib.LinearAlgebra.Span.TensorProduct Mathlib.LinearAlgebra.SpecialLinearGroup Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.Transvection Mathlib.LinearAlgebra.UnitaryGroup Mathlib.LinearAlgebra.Vandermonde Mathlib.Logic.Hydra Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap 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.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.AbsolutelyContinuous Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut 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.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.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas 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.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.MeanValue Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Regular Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Measure.CharacteristicFunction 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.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.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.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.ModelTheory.Graph Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.ArithmeticFunction.Carmichael Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.Chebyshev Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.FermatPsp Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.Instances Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation 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.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.NumberTheory.ModularForms.Cusps Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Modular Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.Niven Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Completion Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Complex Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.Padics.WithVal Mathlib.NumberTheory.PowModTotient Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumFourSquares Mathlib.NumberTheory.SumTwoSquares 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.WellApproximable Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Order.GameAdd Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.SetBernoulli 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.Integration Mathlib.Probability.Kernel.CompProdEqIff Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous Mathlib.Probability.Kernel.Composition.IntegralCompProd 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.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.CovarianceBilin 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.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.RepresentationTheory.AlgebraRepresentation.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FinGroupCharZero Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Irreducible Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.RingTheory.AdicCompletion.RingHom Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Complex Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.DividedPowers.RatAlgebra Mathlib.RingTheory.DividedPowers.SubDPIdeal Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Extension.Basic Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.Generators Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HahnSeries.Binomial Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HopkinsLevitzki Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.KrullsHeightTheorem Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Ideal Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.LinearTopology Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.GeometricallyReduced Mathlib.RingTheory.NoetherNormalization Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.NormTrace Mathlib.RingTheory.NormalClosure Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.BDeRham Mathlib.RingTheory.Perfectoid.FontaineTheta Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.DegreeLT Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Resultant.Basic Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.Polynomial.SmallDegreeVieta Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Binomial Mathlib.RingTheory.PowerSeries.Catalan Mathlib.RingTheory.PowerSeries.CoeffMulMem Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Evaluation Mathlib.RingTheory.PowerSeries.Exp Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.RingTheory.PowerSeries.Ideal Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.PowerSeries.Restricted Mathlib.RingTheory.PowerSeries.Schroder Mathlib.RingTheory.PowerSeries.Substitution Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WeierstrassPreparation Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.QuasiFinite.Basic Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.LocallyStandardSmooth Mathlib.RingTheory.RingHom.QuasiFinite Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Fiber Mathlib.RingTheory.Smooth.Field Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.LTSeries Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Spectrum.Prime.Noetherian Mathlib.RingTheory.Spectrum.Prime.Polynomial Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.TensorProduct.IsBaseChangeHom Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.DiscreteValuativeRel Mathlib.RingTheory.Valuation.FiniteField Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.IntegrallyClosed Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.WittVector.Basic Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.Complete Mathlib.RingTheory.WittVector.Defs Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.Domain Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Frobenius Mathlib.RingTheory.WittVector.Identities Mathlib.RingTheory.WittVector.InitTail Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.WittVector.Isocrystal Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.WittVector.MulP Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.WittVector.TeichmullerSeries Mathlib.RingTheory.WittVector.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.ZMod.Torsion Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.RingTheory.ZariskisMainTheorem Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.PGame.Algebra Mathlib.SetTheory.PGame.Order Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.Surreal.Dyadic Mathlib.SetTheory.Surreal.Multiplication Mathlib.SetTheory.ZFC.Class Mathlib.SetTheory.ZFC.Ordinal Mathlib.SetTheory.ZFC.VonNeumann Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactification.OnePoint.ProjectiveLine Mathlib.Topology.Compactification.OnePoint.Sphere Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.Instances.Matrix Mathlib.Topology.MetricSpace.HausdorffDimension

2

---

Declarations diff

+ _root_.Equiv.sigmaFiberFromRel
+ _root_.Equiv.sigmaQuotFromRel
+ _root_.Equiv.sigmaQuotientFromRel
+ fromRelNdrec
+ mem_fromRel_comap

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[SnirBroshi]

Similar to #34907 I tried to generalize to fibers, and I think it worked :)
I kept the quotient versions since they're not trivial as in that previous PR.