feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes

[yonggyuchoimath]

We prove the following:

• AffineScheme.effectiveEpiOfFlatOfSurjective: A flat surjective morphism (between affine schemes) is an effective epimorphism in the category of affine schemes.
• descSpecOfFlatOfSurjective: Given a morphism e : Spec S ⟶ U of schemes which coequalizes the two projections (Spec S) ×[Spec R] (Spec S) ⟶ Spec S, this constructs a unique morphism Spec R ⟶ U of schemes that e factors through.
• effectiveEpi_Spec_of_flat_of_surjective: If f : R ⟶ S is a flat ring map in CommRingCat with surjective Spec.map f : Spec S ⟶ Spec R, then Spec.map f : Spec S ⟶ Spec R is an effective epimorphism in the category of schemes.

---

• depends on: feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma #30237
• depends on: feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ #30204

Note:

I've again incorporated Scheme.isAffine_local_affine, an instance saying that any Scheme.local_affine at a point gives an affine scheme, in order to define coverR in line 259. As already noted in this review of #30034, having Scheme.local_affine in statements is not desirable as any such statements should be true for any open affine neightborhoods.

In fact, it is possible to define coverR (and prove the rest) without invoking this instance, e.g., using exists_isAffineOpen_mem_and_subset. A problem of this approach is that IsAffine is not automatically synthesized (even if I add an IsAffine instance for exists_isAffineOpen_mem_and_subset) because hxU : x ∈ U can't be synthesized automatically, and this forced to explicitly write down the proof of IsAffine everytime. That's the reason that I included Scheme.isAffine_local_affine in this PR. I would appreciate any suggestions on this.

Another note:

I've marked many definitions and lemmas with private. My criterion was the following:

• It is not optimal as it is stated and can be enhanced after proving effectiveEpi_Spec_of_flat_of_surjective: base_factorization in line 102 (as it should be true for quasi-compact coverings that are flat surjective).
• The definition/lemma seems specific to the proof of descSpecOfFlatOfSurjective. Even when proving fpqc morphisms of algebraic spaces are effective epimorphisms, we would only need descSpecOfFlatOfSurjective and lemmas about it (but not the things like e'_coeq_pullback_f' or desc'_cocycle_condition), cf. Stacks project, Tag 04P2.

[github-actions]

PR summary 71a105d772

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.TensorProduct.Basic	1007	990	-17 (-1.69%)

Import changes for all files

Files	Import difference
5 files Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.Module.Bimodule Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.RingTheory.TensorProduct.Basic	-17
3 files Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Kronecker Mathlib.LinearAlgebra.Matrix.Vec	-16
3 files Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.Quotient	-3
8 files Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Inverse Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.Submodule	-2
50 files Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Lie.Classical Mathlib.Algebra.Lie.Matrix Mathlib.Algebra.Lie.SkewAdjoint Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.LinearAlgebra.CliffordAlgebra.Contraction 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.Determinant 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.Lagrange Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.Orientation Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.UnitaryGroup Mathlib.LinearAlgebra.Vandermonde Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Polynomial.DegreeLT Mathlib.Topology.Algebra.Module.Determinant	-1
1170 files Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Azumaya.Basic Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Topology Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.Solvable 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.FinitePresentation Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Algebra.Module.Presentation.Finite Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Group 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.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.IdealSheaf 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.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.AbsoluteValue.Equivalence 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.Order Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.GelfandDuality 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.FiniteDimension Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable 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.CauchyIntegral Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Harmonic.Analytic Mathlib.Analysis.Complex.Harmonic.MeanValue Mathlib.Analysis.Complex.HasPrimitives Mathlib.Analysis.Complex.JensenFormula Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.MeanValue Mathlib.Analysis.Complex.OpenMapping 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.Manifold Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.ProximityFunction Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle 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.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.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.WeakDual Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.Matrix.Order 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.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Field.WithAbs Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual 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.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.PosPart.Isometric Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric 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.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.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.ErdosGinzburgZiv Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Configuration Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Data.Nat.PowModTotient Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis 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.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.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField 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.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Congruence Mathlib.Geometry.Euclidean.Incenter Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.Projection Mathlib.Geometry.Euclidean.SignedDist Mathlib.Geometry.Euclidean.Sphere.Basic 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.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.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom 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.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.InformationTheory.KullbackLeibler.Basic Mathlib.InformationTheory.KullbackLeibler.KLFun Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Dual.Lemmas 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.FreeModule.Norm Mathlib.LinearAlgebra.JordanChevalley Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.Matrix.BilinearForm 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.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.Rank Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.Matrix.Swap Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.PerfectPairing.Matrix Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.RootSystem.BaseChange 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.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.LinearAlgebra.Trace 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.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.FactorsThrough Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.JacobianOneDim Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.IntegralConvolution Mathlib.MeasureTheory.Group.ModularCharacter Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap Mathlib.MeasureTheory.Integral.CircleAverage Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.CurveIntegral.Basic Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntegrationByParts Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.SetIntegral 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.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.TightNormed Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Order.UpperLower 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.NumberTheory.AbelSummation 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.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.LucasLehmer Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp 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.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion 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.Petersson Mathlib.NumberTheory.ModularForms.QExpansion 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.Embeddings 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.Ideal 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.Complex 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.Measure Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.Wilson Mathlib.NumberTheory.ZetaValues Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity 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.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Uniform Mathlib.Probability.HasLawExists Mathlib.Probability.HasLaw Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.CharacteristicFunction Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.InfinitePi 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.IonescuTulcea.Traj Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.RadonNikodym 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.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.Probability.Variance Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Homological.FiniteCyclic Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro Mathlib.RepresentationTheory.Homological.GroupHomology.Basic Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro Mathlib.RepresentationTheory.Homological.Resolution Mathlib.RepresentationTheory.Induced Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Submodule Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Complex Mathlib.RingTheory.Conductor Mathlib.RingTheory.CotangentLocalizationAway 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.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure 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.Etale.Basic Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension.Basic Mathlib.RingTheory.Extension.Cotangent.Basic 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.Extension Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.Flat.Tensor Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Generators Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.HopkinsLevitzki 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.Ideal.Quotient.Index Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.Invariant Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Jacobson.Artinian Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Polynomial Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Semilocal Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.NoetherNormalization Mathlib.RingTheory.Norm.Basic Mathlib.RingTheory.Norm.Transitivity Mathlib.RingTheory.NormTrace Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.OrderOfVanishing Mathlib.RingTheory.Perfection 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.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.Presentation Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.Flat Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.Bijective Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.SimpleModule.IsAlgClosed Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Spectrum.Maximal.Localization 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.RingHom Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.TensorProduct.Pi 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.Integral Mathlib.RingTheory.Valuation.IntegrallyClosed Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly 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.Teichmuller Mathlib.RingTheory.WittVector.Truncated Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.ZMod.Torsion Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Ring.Compact 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.Compactification.OnePointEquiv Mathlib.Topology.Instances.Matrix Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.Sheaves.CommRingCat	1
Mathlib.RingTheory.TensorProduct.Maps (new file)	1008
Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight (new file)	1597
Mathlib.Algebra.Category.Ring.EqualizerPushout (new file)	1907
Mathlib.AlgebraicGeometry.EffectiveEpi (new file)	2174

---

Declarations diff

+ AffineScheme.effectiveEpiOfFlatOfSurjective
+ ExactIncludeLeftSubRight_desc_faithfullyFlat
+ ExactIncludeLeftSubRight_of_section
+ Scheme.isAffine_local_affine
+ descSpecOfFlatOfSurjective
+ descSpecOfFlatOfSurjective_comp
+ descSpecOfFlatOfSurjective_unique
+ distribBaseChange_includeLeft_lTensor
+ distribBaseChange_includeLeft_lTensor_tmul
+ distribBaseChange_includeRight_lTensor
+ distribBaseChange_includeRight_lTensor_tmul
+ distribBaseChange_symm_tmul
+ distribBaseChange_tmul
+ effectiveEpi_Spec_of_flat_of_surjective
+ effectiveEpi_of_faithfullyFlat
+ equivCommRingCat_functor_map
+ equivCommRingCat_inverse_map
+ exactIncludeLeftSubRight_of_faithfullyFlat
+ flat_and_surjective_iff_faithfullyFlat_of_isAffine
+ forkPushoutCoconeSelf
+ includeLeftSubRight
+ includeLeftSubRight_apply
+ includeLeftSubRight_distribBaseChange
+ includeLeftSubRight_zero_of_mem_range
+ isColimitCoforkSpecPullbackOfFlatOfSurjective
+ isColimitOfπPullbackOfFaithfullyFlat
+ isLimitForkPushoutSelfOfFaithfullyFlat
+ isLimitforkPushoutCoconeSelfOfFaithfullyFlat
+ pushoutCoconeSelf
+ regularEpiOfFaithfullyFlat
+ rid_lTensor
+ toEqLocusOfInclusion
+ toEqLocusOfInclusion_injective
+ toEqLocusOfInclusion_surjective
+ toEqualizerPushoutCoconeSelf
+ toEqualizerPushoutCoconeSelf_bij_of_faithfullyFlat
+ toEqualizerPushoutCoconeSelf_inj_of_inj
+ toEqualizerPushoutCoconeSelf_surj_of_exactIncludeLeftSubRight
++ ExactIncludeLeftSubRight

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma #30237
• feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCatᵒᵖ #30204
  By Dependent Issues (🤖). Happy coding!