[Merged by Bors] - chore: delete declarations deprecated between 2024-01 and 2024-07 by YaelDillies · Pull Request #21271 · leanprover-community/mathlib4

YaelDillies · 2025-01-30T18:29:36Z

The first commit was done by replacing all matches of @\[deprecated.*\(since := "2024-0[1-7]-.."\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n? with nothing. The second commit was done manually.

github-actions · 2025-01-30T18:30:36Z

PR summary b8844fc5d8

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Deprecated.Combinator	18	0	-18 (-100.00%)
Mathlib.Deprecated.HashMap	22	0	-22 (-100.00%)
Mathlib.Deprecated.LazyList	387	0	-387 (-100.00%)
Mathlib.Deprecated.RelClasses	111	0	-111 (-100.00%)
Mathlib.Topology.Order.Bounded	1116	0	-1116 (-100.00%)
Mathlib.Deprecated.AlgebraClasses	47	18	-29 (-61.70%)
Mathlib.Deprecated.Aliases	19	18	-1 (-5.26%)
Mathlib.Algebra.Algebra.Spectrum	1032	1003	-29 (-2.81%)
Mathlib.NumberTheory.Zsqrtd.Basic	1095	1079	-16 (-1.46%)
Mathlib.NumberTheory.Zsqrtd.GaussianInt	1134	1118	-16 (-1.41%)
Mathlib.LinearAlgebra.Prod	769	759	-10 (-1.30%)
Mathlib.Algebra.Algebra.Quasispectrum	1034	1021	-13 (-1.26%)
Mathlib.Algebra.TrivSqZeroExt	794	787	-7 (-0.88%)
Mathlib.Algebra.Star.Module	836	829	-7 (-0.84%)
Mathlib.Algebra.DirectSum.Internal	995	988	-7 (-0.70%)
Mathlib.RingTheory.Derivation.Basic	1026	1019	-7 (-0.68%)
Mathlib.RepresentationTheory.FDRep	1698	1692	-6 (-0.35%)
Mathlib.Algebra.Lie.Weights.Linear	1868	1863	-5 (-0.27%)
Mathlib.Order.OmegaCompletePartialOrder	415	414	-1 (-0.24%)
Mathlib.Control.LawfulFix	497	496	-1 (-0.20%)
Mathlib.RingTheory.Int.Basic	1065	1063	-2 (-0.19%)
Mathlib.RingTheory.FractionalIdeal.Basic	1087	1085	-2 (-0.18%)
Mathlib.LinearAlgebra.FiniteDimensional.Defs	1168	1166	-2 (-0.17%)
Mathlib.Topology.ContinuousMap.Algebra	1180	1178	-2 (-0.17%)
Mathlib.GroupTheory.Nilpotent	1200	1198	-2 (-0.17%)
Mathlib.RingTheory.IntegralDomain	1235	1233	-2 (-0.16%)
Mathlib.LinearAlgebra.BilinearForm.Orthogonal	1266	1264	-2 (-0.16%)
Mathlib.LinearAlgebra.Matrix.ZPow	1314	1312	-2 (-0.15%)
Mathlib.Analysis.Asymptotics.Lemmas	1322	1320	-2 (-0.15%)
Mathlib.Analysis.NormedSpace.Int	1326	1324	-2 (-0.15%)
Mathlib.Analysis.SpecificLimits.Normed	1413	1411	-2 (-0.14%)
Mathlib.Topology.Algebra.Module.Multilinear.Topology	1413	1411	-2 (-0.14%)
Mathlib.Analysis.Normed.Group.AddCircle	1447	1445	-2 (-0.14%)
Mathlib.NumberTheory.Padics.PadicIntegers	1459	1457	-2 (-0.14%)
Mathlib.Analysis.Complex.Basic	1463	1461	-2 (-0.14%)
Mathlib.NumberTheory.Padics.RingHoms	1475	1473	-2 (-0.14%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf	1507	1505	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Exp	1520	1518	-2 (-0.13%)
Mathlib.Analysis.Complex.Circle	1523	1521	-2 (-0.13%)
Mathlib.LinearAlgebra.BilinearForm.Basic	762	761	-1 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Log.Basic	1528	1526	-2 (-0.13%)
Mathlib.Analysis.Calculus.FDeriv.Add	1543	1541	-2 (-0.13%)
Mathlib.Analysis.Calculus.LocalExtr.Basic	1546	1544	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle	1578	1576	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Pow.Complex	1584	1582	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Pow.Real	1585	1583	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Pow.NNReal	1586	1584	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Complex.Circle	1587	1585	-2 (-0.13%)
Mathlib.Analysis.SpecialFunctions.Log.Base	1587	1585	-2 (-0.13%)
Mathlib.Analysis.PSeries	1590	1588	-2 (-0.13%)
Mathlib.Analysis.Normed.Lp.lpSpace	1621	1619	-2 (-0.12%)
Mathlib.Analysis.CStarAlgebra.Multiplier	1640	1638	-2 (-0.12%)
Mathlib.RingTheory.Localization.Basic	840	839	-1 (-0.12%)
Mathlib.LinearAlgebra.BilinearForm.Hom	866	865	-1 (-0.12%)
Mathlib.Geometry.Manifold.MFDeriv.Defs	1776	1774	-2 (-0.11%)
Mathlib.Analysis.Calculus.FDeriv.Extend	1799	1797	-2 (-0.11%)
Mathlib.Algebra.Algebra.Subalgebra.Basic	936	935	-1 (-0.11%)
Mathlib.RingTheory.Localization.NumDen	936	935	-1 (-0.11%)
Mathlib.Geometry.Manifold.Instances.Real	1881	1879	-2 (-0.11%)
Mathlib.Algebra.Vertex.HVertexOperator	947	946	-1 (-0.11%)
Mathlib.MeasureTheory.Integral.IntegrableOn	1905	1903	-2 (-0.10%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp	1906	1904	-2 (-0.10%)
Mathlib.MeasureTheory.Function.UniformIntegrable	1907	1905	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.Bochner	1909	1907	-2 (-0.10%)
Mathlib.Probability.Kernel.Integral	1913	1911	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ContinuousMapDense	1917	1915	-2 (-0.10%)
Mathlib.Geometry.Manifold.Instances.Sphere	1935	1933	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.SetIntegral	1943	1941	-2 (-0.10%)
Mathlib.MeasureTheory.Group.FundamentalDomain	1950	1948	-2 (-0.10%)
Mathlib.MeasureTheory.Function.L2Space	1955	1953	-2 (-0.10%)
Mathlib.MeasureTheory.Function.AEEqOfIntegral	1961	1959	-2 (-0.10%)
Mathlib.Analysis.Convex.Integral	1963	1961	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique	1965	1963	-2 (-0.10%)
Mathlib.RingTheory.Ideal.Operations	985	984	-1 (-0.10%)
Mathlib.MeasureTheory.Decomposition.RadonNikodym	1971	1969	-2 (-0.10%)
Mathlib.Probability.Kernel.Disintegration.CDFToKernel	1971	1969	-2 (-0.10%)
Mathlib.MeasureTheory.Measure.Tilted	1972	1970	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2	1977	1975	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1	1978	1976	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic	1979	1977	-2 (-0.10%)
Mathlib.Probability.Kernel.Disintegration.CondCDF	1982	1980	-2 (-0.10%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.Real	1994	1992	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.IntervalIntegral	1995	1993	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.DominatedConvergence	1996	1994	-2 (-0.10%)
Mathlib.Probability.Process.Filtration	1996	1994	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.Prod	1997	1995	-2 (-0.10%)
Mathlib.Probability.IdentDistrib	1997	1995	-2 (-0.10%)
Mathlib.Probability.Martingale.Basic	2000	1998	-2 (-0.10%)
Mathlib.Probability.Kernel.Composition.IntegralCompProd	2002	2000	-2 (-0.10%)
Mathlib.MeasureTheory.Measure.Haar.NormedSpace	2004	2002	-2 (-0.10%)
Mathlib.Probability.Kernel.Composition.MeasureCompProd	2008	2006	-2 (-0.10%)
Mathlib.Probability.Density	2009	2007	-2 (-0.10%)
Mathlib.Probability.Martingale.Convergence	2011	2009	-2 (-0.10%)
Mathlib.Probability.Martingale.BorelCantelli	2015	2013	-2 (-0.10%)
Mathlib.Probability.Kernel.Disintegration.Density	2019	2017	-2 (-0.10%)
Mathlib.Algebra.Polynomial.AlgebraMap	1010	1009	-1 (-0.10%)
Mathlib.Probability.Kernel.RadonNikodym	2021	2019	-2 (-0.10%)
Mathlib.Algebra.Polynomial.Smeval	1013	1012	-1 (-0.10%)
Mathlib.RingTheory.Localization.Away.Basic	1016	1015	-1 (-0.10%)
Mathlib.FieldTheory.IntermediateField.Basic	1026	1025	-1 (-0.10%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs	1027	1026	-1 (-0.10%)
Mathlib.Probability.Kernel.Disintegration.StandardBorel	2064	2062	-2 (-0.10%)
Mathlib.Probability.Kernel.Disintegration.Integral	2065	2063	-2 (-0.10%)
Mathlib.Probability.Kernel.CondDistrib	2067	2065	-2 (-0.10%)
Mathlib.Analysis.SpecialFunctions.PolarCoord	2100	2098	-2 (-0.10%)
Mathlib.MeasureTheory.Integral.IntegralEqImproper	2125	2123	-2 (-0.09%)
Mathlib.Analysis.FunctionalSpaces.SobolevInequality	2139	2137	-2 (-0.09%)
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls	2159	2157	-2 (-0.09%)
Mathlib.NumberTheory.LSeries.RiemannZeta	2274	2272	-2 (-0.09%)
Mathlib.MeasureTheory.OuterMeasure.Caratheodory	1318	1317	-1 (-0.08%)
Mathlib.MeasureTheory.Measure.MeasureSpace	1332	1331	-1 (-0.08%)
Mathlib.MeasureTheory.Measure.Typeclasses	1340	1339	-1 (-0.07%)
Mathlib.Dynamics.Ergodic.Ergodic	1349	1348	-1 (-0.07%)
Mathlib.MeasureTheory.Integral.Lebesgue	1403	1402	-1 (-0.07%)
Mathlib.MeasureTheory.Measure.WithDensity	1405	1404	-1 (-0.07%)
Mathlib.Probability.Kernel.Defs	1405	1404	-1 (-0.07%)
Mathlib.Probability.Kernel.Basic	1406	1405	-1 (-0.07%)
Mathlib.Probability.Kernel.MeasurableLIntegral	1407	1406	-1 (-0.07%)
Mathlib.Probability.Kernel.Composition.Basic	1410	1409	-1 (-0.07%)
Mathlib.MeasureTheory.Function.AEEqOfLIntegral	1449	1448	-1 (-0.07%)
Mathlib.MeasureTheory.Function.LpSeminorm.Basic	1664	1663	-1 (-0.06%)
Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov	1665	1664	-1 (-0.06%)
Mathlib.MeasureTheory.Function.LpSeminorm.Trim	1665	1664	-1 (-0.06%)
Mathlib.MeasureTheory.Integral.MeanInequalities	1680	1679	-1 (-0.06%)
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp	1698	1697	-1 (-0.06%)
Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality	1698	1697	-1 (-0.06%)
Mathlib.MeasureTheory.Function.LpSpace	1743	1742	-1 (-0.06%)
Mathlib.MeasureTheory.Function.ConvergenceInMeasure	1745	1744	-1 (-0.06%)

Import changes for all files

Files	Import difference
`Mathlib.Topology.Order.Bounded`	-1116
`Mathlib.Deprecated.LazyList`	-387
`Mathlib.Deprecated.RelClasses`	-111
`Mathlib.Algebra.Algebra.Spectrum` `Mathlib.Deprecated.AlgebraClasses`	-29
`Mathlib.Algebra.Star.Unitary`	-25
`Mathlib.Deprecated.HashMap`	-22
`Mathlib.Topology.Algebra.Module.CharacterSpace`	-21
`Mathlib.Deprecated.Combinator`	-18
4 files `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.GaussianInt`	-16
`Mathlib.NumberTheory.Zsqrtd.ToReal`	-15
`Mathlib.Algebra.Algebra.Quasispectrum`	-13
`Mathlib.Topology.ContinuousMap.Units`	-12
6 files `Mathlib.Algebra.Module.Injective` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.LinearAlgebra.Prod` `Mathlib.LinearAlgebra.TensorProduct.Prod`	-10
4 files `Mathlib.Algebra.Lie.Sl2` `Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.NumberTheory.Pell`	-8
162 files `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Algebra.Category.AlgebraCat.Basic` `Mathlib.Algebra.Category.AlgebraCat.Monoidal` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.CharP.Subring` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Module.Projective` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Star.Module` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Convex.Basic` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Join` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Segment` `Mathlib.Analysis.Convex.Slope` `Mathlib.Analysis.Convex.Star` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Data.Complex.Module` `Mathlib.Data.Matrix.Auto` `Mathlib.Data.Matrix.Basic` `Mathlib.Data.Matrix.Basis` `Mathlib.Data.Matrix.Bilinear` `Mathlib.Data.Matrix.Block` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.Data.Matrix.Composition` `Mathlib.Data.Matrix.ConjTranspose` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Data.Matrix.Hadamard` `Mathlib.Data.Matrix.Invertible` `Mathlib.Data.Matrix.Notation` `Mathlib.Data.Matrix.Reflection` `Mathlib.Data.Matrix.RowCol` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.LinearAlgebra.AffineSpace.MidpointZero` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.LinearAlgebra.AffineSpace.Ordered` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.LinearIndependent` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.LinearAlgebra.Pi` `Mathlib.LinearAlgebra.Ray` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.LinearAlgebra.TensorPower.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.AlgebraTower` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Module` `Mathlib.RingTheory.MatrixAlgebra` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.TensorProduct.Pi`	-7
46 files `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.KummerExtension` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.LocallyConstant.Algebra`	-6
19 files `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Colimit.Module` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity`	-5
6 files `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors`	-4
4 files `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.PowerSeries.Order`	-3
1321 files `Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.Ring` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.Exact` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.Algebra.Module.Presentation.Basic` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.Algebra.Module.Presentation.RestrictScalars` `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.Algebra.Module.Presentation.Tensor` `Mathlib.Algebra.Module.SnakeLemma` `Mathlib.Algebra.Module.Torsion` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Algebra.Module.ZMod` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Algebra.Order.AbsoluteValue.Equivalence` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.Analysis.Analytic.IteratedFDeriv` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.Meromorphic` `Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `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.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Deriv.Pi` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Analysis.Calculus.Deriv.Prod` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.Analysis.Calculus.Deriv.Star` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.FDeriv.WithLp` `Mathlib.Analysis.Calculus.FirstDerivativeTest` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Between` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.Pointed` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Exposed` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convex.Normed` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Convex.Radon` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Convex.Visible` `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.FourierTransformDeriv` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WeakOperatorTopology` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.MeanInequalities` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.Norm` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.InfiniteSum` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.IsPowMulFaithful` `Mathlib.Analysis.Normed.Ring.SeminormFromBounded` `Mathlib.Analysis.Normed.Ring.SeminormFromConst` `Mathlib.Analysis.Normed.Ring.Seminorm` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Basic` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.Injective` `Mathlib.CategoryTheory.Abelian.ProjectiveDimension` `Mathlib.CategoryTheory.Abelian.Projective` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.CauchyDavenport` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Condensed.AB` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Epi` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.AB` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Data.Complex.Cardinality` `Mathlib.Data.Complex.Determinant` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Data.Complex.Orientation` `Mathlib.Data.Matrix.DoublyStochastic` `Mathlib.Data.Matrix.Kronecker` `Mathlib.Data.Matrix.Rank` `Mathlib.Data.Nat.Factorial.SuperFactorial` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Data.ZMod.Coprime` `Mathlib.Data.ZMod.QuotientGroup` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Dynamics.Newton` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.FieldTheory.RatFunc.Basic` `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.Affine` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `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.AnalyticManifold` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiff.Product` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.IsManifold.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.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `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.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorField` `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.CosetCover` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.GroupTheory.Frattini` `Mathlib.GroupTheory.Nilpotent` `Mathlib.GroupTheory.Order.Min` `Mathlib.GroupTheory.PGroup` `Mathlib.GroupTheory.Schreier` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.GroupTheory.Sylow` `Mathlib.GroupTheory.Torsion` `Mathlib.GroupTheory.Transfer` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.LinearAlgebra.BilinearForm.Properties` `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.Star` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.LinearAlgebra.Contraction` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.LinearAlgebra.Dual` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.LinearAlgebra.ExteriorPower.Basic` `Mathlib.LinearAlgebra.ExteriorPower.Pairing` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.Goursat` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `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.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.LinearAlgebra.Matrix.Determinant.Misc` `Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Matrix.IsDiag` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.LinearAlgebra.Orientation` `Mathlib.LinearAlgebra.PerfectPairing.Basic` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.Projection` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `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` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.Reflection` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.LinearAlgebra.TensorPower.Pairing` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.LinearAlgebra.Vandermonde` `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.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `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.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.MeasureTheory.Function.Intersectivity` `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.Inner` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `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.Integral` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntervalAverage` `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.SetToL1` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `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.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.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.FLT.Four` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `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.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.Integrable` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Integration` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.Lemmas` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.MeasureComp` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.Basic` `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.MeasurableIntegral` `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.IntegrableExpMul` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.StrongLaw` `Mathlib.Probability.Variance` `Mathlib.RepresentationTheory.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RepresentationTheory.Rep` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.Extension` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.RingTheory.Finiteness.TensorProduct` `Mathlib.RingTheory.Flat.Basic` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Flat.Equalizer` `Mathlib.RingTheory.Flat.FaithfullyFlat.Basic` `Mathlib.RingTheory.Flat.Localization` `Mathlib.RingTheory.Flat.Stability` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.Generators` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.HopfAlgebra` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.MinimalPrime` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.IntegralDomain` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.Norm.Defs` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.PowerSeries.Binomial` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.PowerSeries.PiTopology` `Mathlib.RingTheory.Presentation` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.SimpleModule` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.RingTheory.ZMod` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.ContinuousMonoidHom` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.CWComplex` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.CompHaus.Frm` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Topology.Category.Compactum` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Topology.Category.Locale` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Compactification.OnePointEquiv` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.Germ` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.HolderNorm` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom`	-2
245 files `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Tower` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Module.LocalizedModule.Basic` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Module.LocalizedModule.IsLocalization` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Algebra.RingQuot` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.Algebra.Star.RingQuot` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Control.LawfulFix` `Mathlib.Deprecated.Aliases` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.Span.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.LinearAlgebra.Trace` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.MeasureTheory.Function.LpSpace` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.Multiplicity` `Mathlib.Order.Category.OmegaCompletePartialOrder` `Mathlib.Order.CompletePartialOrder` `Mathlib.Order.OmegaCompletePartialOrder` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Kernel.Basic` `Mathlib.Probability.Kernel.Composition.Basic` `Mathlib.Probability.Kernel.Composition.CompNotation` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.Probability.Kernel.Proper` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.UniformOn` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Maximal` `Mathlib.RingTheory.Ideal.Nonunits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Span` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.Basic` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.Spectrum.Maximal.Basic` `Mathlib.RingTheory.Spectrum.Maximal.Defs` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.Tactic.Algebraize` `Mathlib.Tactic.Module` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.OmegaCompletePartialOrder` `Mathlib.Topology.Sheaves.Alexandrov`	-1

Declarations diff

- AEEqFun.snorm_compMeasurePreserving
- AEFinStronglyMeasurable.ae_eq_of_forall_set_integral_eq
- AEFinStronglyMeasurable.ae_eq_zero_of_forall_set_integral_eq_zero
- AEFinStronglyMeasurable.ae_nonneg_of_forall_set_integral_nonneg
- AEMeasurable.ae_eq_of_forall_set_lintegral_eq
- AbsoluteValue.map_units_int_cast
- AddMonoid.End.int_cast_apply
- AffineTargetMorphismProperty.diagonalOfTargetAffineLocally
- Antivary.sum_mul_eq_sum_comp_perm_mul_iff
- Antivary.sum_smul_eq_sum_comp_perm_smul_iff
- Antivary.sum_smul_eq_sum_smul_comp_perm_iff
- AntivaryOn.sum_mul_eq_sum_comp_perm_mul_iff
- AntivaryOn.sum_smul_eq_sum_comp_perm_smul_iff
- AntivaryOn.sum_smul_eq_sum_smul_comp_perm_iff
- Bijective.Prod_map
- BilinForm.toLin_apply
- BilinForm.toLin_symm
- C_eq_int_cast
- C_eq_nat_cast
- CancelVAdd
- CategoryTheory.FreeMonoidalCategory.discrete_functor_map_eq_id
- CategoryTheory.FreeMonoidalCategory.discrete_functor_obj_eq_as
- CategoryTheory.Functor.map_exact
- CompactT2.projective_iff_extremallyDisconnnected
- CompleteLatticeHom.apply_liminf_iterate
- CompleteLatticeHom.apply_limsup_iterate
- Continuous
- Continuous'
- Continuous'.to_bundled
- Continuous'.to_monotone
- Continuous.exp
- Continuous.of_bundled
- Continuous.of_bundled'
- ContinuousAt.exp
- ContinuousOn.exp
- ContinuousWithinAt.exp
- CovBy.cast_int
- Equiv
- Equiv.piFinCastSucc
- Equiv.piFinSucc
- Equiv.piFinSuccAbove
- EssSurj
- Euclidean_space.volume_ball
- Euclidean_space.volume_closedBall
- Even.zsmul
- Even.zsmul'
- Faithful
- Faithful.div
- Faithful.div_comp
- Faithful.div_faithful
- Faithful.of_comp
- Faithful.of_comp_eq
- Faithful.of_comp_iso
- Faithful.of_iso
- FdRep
- Filter.Eventually.int_cast_atBot
- Filter.Eventually.int_cast_atTop
- Filter.Eventually.nat_cast_atTop
- Filter.Eventually.rat_cast_atBot
- Filter.Eventually.rat_cast_atTop
- Filter.isBounded_ge_map_of_bounded_range
- Filter.isBounded_le_map_of_bounded_range
- Full
- Full.ofCompFaithful
- Full.ofCompFaithfulIso
- Full.ofIso
- Functor.image_preimage
- Group.one_lt_exponent
- HasCompactSupport.smul_left'
- HasFiniteIntegral.tendsto_set_integral_nhds_zero
- I
- InfHom.le_apply_bliminf
- Injective.Prod_map
- Int.coe_nat_multiplicity
- Int.coe_nat_pow_pred
- Int.smul_one_eq_coe
- IntValuation.le_max_iff_min_le
- IntValuation.map_add_le_max'
- IntValuation.map_mul'
- IntValuation.map_one'
- IntValuation.map_zero'
- Integrable.ae_eq_of_forall_set_integral_eq
- Integrable.ae_eq_zero_of_forall_set_integral_eq_zero
- Integrable.tendsto_set_integral_nhds_zero
- Integrable.tendsto_snorm_condExp
- Integrable.tendsto_snorm_condexp
- IntegrableOn.set_lintegral_lt_top
- Involutive.Prod_map
- IsAffineOpen.basicOpenIsAffine
- IsAffineOpen.fromSpec_base_preimage
- IsAffineOpen.fromSpec_map_basicOpen
- IsAffineOpen.fromSpec_map_basicOpen'
- IsAffineOpen.fromSpec_range
- IsAffineOpen.imageIsOpenImmersion
- IsAffineOpen.mapRestrictBasicOpen
- IsAffineOpen.opensFunctor_map_basicOpen
- IsBigO.nat_cast_atTop
- IsCondKernelCDF.set_lintegral
- IsCoverDense.sheafEquivOfCoverPreservingCoverLifting
- IsCoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility
- IsCyclotomicExtension.isPrimePow_norm_zeta_sub_one
- IsCyclotomicExtension.prime_ne_two_norm_zeta_sub_one
- IsCyclotomicExtension.two_pow_norm_zeta_sub_one
- IsEquivalence
- IsEquivalence.cancelCompLeft
- IsEquivalence.cancelCompRight
- IsEquivalence.equivOfIso
- IsEquivalence.fun_inv_map
- IsEquivalence.inv_fun_map
- IsEquivalence.ofIso
- IsEquivalence.ofIso_refl
- IsEquivalence.ofIso_trans
- IsIncompTrans
- IsLinearOrder.swap
- IsLittleO.nat_cast_atTop
- IsNontrivial.comp
- IsNontrivial.sum_eq_zero
- IsPrimitiveRoot.pow_sub_one_norm_prime_ne_two
- IsPrimitiveRoot.pow_sub_one_norm_prime_pow_ne_two
- IsPrimitiveRoot.pow_sub_one_norm_prime_pow_of_ne_zero
- IsPrimitiveRoot.pow_sub_one_norm_two
- IsPrimitiveRoot.sub_one_norm_prime
- IsPrimitiveRoot.sub_one_norm_prime_ne_two
- IsPrimitiveRoot.sub_one_norm_two
- IsProperMap.closed_range
- IsRatCondKernelCDFAux.set_integral_iInf_rat_gt
- IsTotalPreorder
- IsTotalPreorder.swap
- Iso.map_essSurj
- K
- LT.lt.eq_bot
- LT.lt.eq_top
- LeftInverse.Prod_map
- Limits.baseChange
- LinearMap.BilinForm.toLin
- LinearMap.toBilin
- LinearMap.toBilinAux
- LinearMap.toBilinAux_eq
- LinearMap.toBilin_apply
- LinearMap.toBilin_symm
- LocallyRingedSpace.toΓSpec_preim_basicOpen_eq
- Lp.ae_eq_of_forall_set_integral_eq
- Lp.ae_eq_of_forall_set_integral_eq'
- Lp.ae_eq_zero_of_forall_set_integral_eq_zero
- Lp.ae_eq_zero_of_forall_set_integral_eq_zero'
- Martingale.eq_condExp_of_tendsto_snorm
- Martingale.eq_condexp_of_tendsto_snorm
- MeasurePreserving.set_integral_image_emb
- MeasurePreserving.set_integral_preimage_emb
- MeasurePreserving.set_lintegral_comp_emb
- MeasurePreserving.set_lintegral_comp_preimage
- MeasurePreserving.set_lintegral_comp_preimage_emb
- Memℒp.exists_boundedContinuous_snorm_sub_le
- Memℒp.exists_hasCompactSupport_snorm_sub_le
- Memℒp.exists_snorm_indicator_compl_lt
- Memℒp.snormEssSup_indicator_norm_ge_eq_zero
- Memℒp.snorm_eq_integral_rpow_norm
- Memℒp.snorm_indicator_le
- Memℒp.snorm_indicator_le'
- Memℒp.snorm_indicator_le_of_meas
- Memℒp.snorm_indicator_norm_ge_le
- Memℒp.snorm_indicator_norm_ge_pos_le
- Memℒp.snorm_lt_top
- Memℒp.snorm_mk_lt_top
- Memℒp.snorm_ne_top
- Module.Finite.injective_of_surjective_endomorphism
- Nat.cast_int_covBy_iff
- Nat.smul_one_eq_coe
- NormedRing.summable_geometric_of_norm_lt_one
- NormedRing.tsum_geometric_of_norm_lt_one
- OpenCover.Covers
- OrderIso.apply_bliminf
- OrderIso.apply_blimsup
- OrderIso.piFinSuccAboveIso
- OrderedCancelVAdd
- OrderedVAdd
- PSigma.lex_wf
- PSigma.revLex_wf
- PSigma.skipLeft_wf
- PrimeSpectrum.IsPrime
- Prod_map
- Proj.stalkIso'_germ'
- RCLike.interval_integral_ofReal
- ReflectsIsomorphisms
- RespectsIso.arrow_iso_iff
- RespectsIso.arrow_mk_iso_iff
- RespectsIso.cancel_left_isIso
- RespectsIso.cancel_right_isIso
- RespectsIso.isoClosure_eq
- RightInverse.Prod_map
- S
- Scheme.affineBasisCoverIsAffine
- Scheme.affineCoverIsAffine
- Scheme.openCoverOfSuprEqTop
- Scheme.quasi_compact_of_affine
- ScottContinuous.continuous'
- Set.restrictPreimage_isClosedMap
- Set.restrictPreimage_isOpenMap
- SetLike.int_cast_mem_graded
- SetLike.nat_cast_mem_graded
- SpecIsAffine
- Squarefree.nodup_factors
- Subalgebra.finiteDimensional_bot
- Submartingale.stoppedValue_leastGE_snorm_le
- Submartingale.stoppedValue_leastGE_snorm_le'
- Submartingale.tendsto_snorm_one_limitProcess
- Submodule.Quotient.isNoetherian
- Sum.uniformSpace
- SupHom.apply_blimsup_le
- Surjective.Prod_map
- Tendsto.atBot_mul_neg_const
- Tendsto.atBot_mul_neg_const'
- Tendsto.atTop_mul_neg_const
- Tendsto.atTop_mul_neg_const'
- Tendsto.neg_const_mul_atBot
- Tendsto.neg_const_mul_atTop
- WithBot.csSup_empty
- Yeq_of_Xeq
- Yeq_of_Yne
- _root_.Antitone.tendsto_set_integral
- _root_.CategoryTheory.Exact.lift
- _root_.CategoryTheory.Exact.lift_comp
- _root_.CategoryTheory.Injective.Exact.comp_desc
- _root_.CategoryTheory.Injective.Exact.desc
- _root_.CategoryTheory.mem_essImage_of_unit_isIso
- _root_.ClosedEmbedding.set_integral_map
- _root_.IsClosedEmbedding.set_integral_map
- _root_.Measurable.set_lintegral_kernel
- _root_.Measurable.set_lintegral_kernel_prod_left
- _root_.Measurable.set_lintegral_kernel_prod_right
- _root_.MeasurableEmbedding.set_integral_map
- _root_.MeasurableEmbedding.snormEssSup_map_measure
- _root_.MeasurableEmbedding.snorm_map_measure
- _root_.MeasureTheory.Measure.compProd_fst_condKernel
- _root_.MeasureTheory.Measure.condKernel_apply_of_ne_zero_of_measurableSet
- _root_.MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt
- _root_.MvPolynomial.degree
- _root_.MvPolynomial.degree_eq_zero_iff
- _root_.MvPolynomial.weightedDegree
- _root_.MvPolynomial.weightedDegree_apply
- _root_.MvPolynomial.weightedDegree_one
- _root_.Nat.cocompact_eq
- _root_.VertexAlg.HetVertexOperator.ext
- _root_.VertexAlg.HetVertexOperator.of_coeff
- _root_.VertexAlg.coeff
- _root_.VertexAlg.coeff_inj
- _root_.VertexAlg.coeff_isPWOsupport
- _root_.abs_coe_circle
- _root_.algebraMap_rat_rat
- _root_.arg_expMapCircle
- _root_.coe_div_circle
- _root_.coe_inv_circle
- _root_.coe_inv_circle_eq_conj
- _root_.expMapCircle
- _root_.expMapCircle_add_two_pi
- _root_.expMapCircle_apply
- _root_.expMapCircle_arg
- _root_.expMapCircle_eq_expMapCircle
- _root_.expMapCircle_sub
- _root_.expMapCircle_sub_two_pi
- _root_.expMapCircle_two_pi
- _root_.expMapCircle_zero
- _root_.int_cast_memℓp_infty
- _root_.invOn_arg_expMapCircle
- _root_.leftInverse_expMapCircle_arg
- _root_.nat_cast_memℓp_infty
- _root_.ne_zero_of_mem_circle
- _root_.normSq_eq_of_mem_circle
- _root_.norm_circle_smul
- _root_.periodic_expMapCircle
- _root_.surjOn_expMapCircle_neg_pi_pi
- abs_coe_nat
- abs_coe_nat_norm
- addY'
- add_def
- add_eq_zero_iff
- add_eq_zero_iff'
- add_halves'
- adjoin_int
- adjoin_nat
- ae_bdd_liminf_atTop_of_snorm_bdd
- ae_bdd_liminf_atTop_rpow_of_snorm_bdd
- ae_empty_or_univ'
- ae_eq_condExp_of_forall_set_integral_eq
- ae_eq_condexp_of_forall_set_integral_eq
- ae_eq_const_or_norm_set_integral_lt_of_norm_le_const
- ae_eq_of_forall_set_integral_eq_of_sigmaFinite
- ae_eq_of_forall_set_integral_eq_of_sigmaFinite'
- ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite
- ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite₀
- ae_eq_restrict_of_forall_set_integral_eq
- ae_eq_zero_of_forall_set_integral_eq_of_finStronglyMeasurable_trim
- ae_eq_zero_of_forall_set_integral_eq_of_sigmaFinite
- ae_eq_zero_of_forall_set_integral_isClosed_eq_zero
- ae_eq_zero_of_snorm'_eq_zero
- ae_eq_zero_restrict_of_forall_set_integral_eq_zero
- ae_eq_zero_restrict_of_forall_set_integral_eq_zero_real
- ae_le_of_forall_set_integral_le
- ae_le_of_forall_set_lintegral_le_of_sigmaFinite
- ae_le_of_forall_set_lintegral_le_of_sigmaFinite₀
- ae_le_snormEssSup
- ae_nonneg_of_forall_setIntegral_nonneg_of_stronglyMeasurable
- ae_nonneg_of_forall_set_integral_nonneg
- ae_nonneg_of_forall_set_integral_nonneg_of_sigmaFinite
- ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable
- ae_nonneg_restrict_of_forall_set_integral_nonneg
- ae_nonneg_restrict_of_forall_set_integral_nonneg_inter
- ae_tendsto_of_cauchy_snorm
- ae_tendsto_of_cauchy_snorm'
- aeval_nat_cast
- affine_cancel_left_isIso
- affine_cancel_right_isIso
- algebraMap_surjective_of_isAlgebraic
- arg_expMapCircle
- asString_inv_toList
- attach_map_coe'
- attach_map_val'
- ball_congr
- baseChange
- baseChange_addY'
- bex_congr
- bex_eq_left
- biUnion_null_iff
- bind
- bind_continuous'
- bind_singleton
- bot_continuous
- bot_ne_nat
- card_congr
- card_divisors
- card_eq_coe_nat_card
- card_fiber_eq_of_mem_range
- card_le_card_of_inj_on
- card_support_cycleOf_pos_iff
- cases
- cases_on
- cases_true_false
- castIso
- castIso_refl
- castIso_to_equiv
- cast_eq_cast_iff_Nat
- cast_int_cast
- cast_int_cast'
- cast_int_comp
- cast_int_left
- cast_int_mul_self
- cast_int_right
- cast_nat_cast
- cast_nat_cast'
- cast_nat_eq_last
- cast_nat_mul_cast_nat_mul
- cast_nat_mul_left
- cast_nat_mul_right
- cast_nat_mul_self
- ceil_logb_nat_cast
- choose_nat_cast
- circle
- coeFn_congr
- coeLazyList
- coe_add
- coe_and_iff
- coe_cast_hom
- coe_decide
- coe_expMapCircle
- coe_int_add
- coe_int_den
- coe_int_div
- coe_int_div_eq_divInt
- coe_int_div_self
- coe_int_dvd
- coe_int_dvd_coe_int
- coe_int_dvd_iff
- coe_int_eq
- coe_int_eq_divInt
- coe_int_im
- coe_int_inj
- coe_int_mul
- coe_int_mul_eq_zsmul
- coe_int_num
- coe_int_re
- coe_int_sub
- coe_int_val
- coe_lt_coe_nat
- coe_natAbs
- coe_nat_div_self
- coe_nat_dvd
- coe_nat_dvd_left
- coe_nat_dvd_right
- coe_nat_ediv
- coe_nat_eq_divInt
- coe_nat_eq_zero
- coe_nat_gcd
- coe_nat_im
- coe_nat_lt_coe
- coe_nat_modEq_iff
- coe_nat_mul_eq_nsmul
- coe_nat_ne_zero
- coe_nat_ne_zero_iff_pos
- coe_nat_nonneg
- coe_nat_nonpos_iff
- coe_nat_pos
- coe_nat_pow
- coe_nat_re
- coe_nat_strictMono
- coe_nat_sub
- coe_nat_succ_pos
- coe_nat_val
- coe_neg
- coe_nnnorm_ae_le_snormEssSup
- coe_or_iff
- coe_pred_of_pos
- coe_rat_mem
- coe_sub
- coe_zero
- coeff_int_cast_ite
- coeff_mem_frange
- coeff_nat_cast_ite
- compProd_fst_condKernel
- compProd_fst_condKernelBorel
- compProd_fst_condKernelCountable
- compProd_fst_condKernelUnitBorel
- compProd_fst_condKernelUnitReal
- comp_val_c_app
- comp_val_c_app_assoc
- cond_decide_mod_two
- conj_nat_cast
- consVal
- cons_sublist_cons_iff
- const_continuous'
- contMDiff_expMapCircle
- continuous'_coe
- continuousAt_removeNth
- continuous_comp
- continuous_const
- continuous_eval_left
- continuous_id
- continuous_set_integral
- cpow_int_cast
- cpow_nat_cast
- decide_False
- decide_True
- decide_not
- degree_int_cast_le
- degree_nat_cast_le
- den_div_cast_eq_one_iff
- denseRange_int_cast
- denseRange_nat_cast
- densely_ordered_iff_forall_not_covBy
- derivative_int_cast
- derivative_int_cast_mul
- derivative_nat_cast
- derivative_nat_cast_mul
- diagonalTargetAffineLocallyOfOpenCover
- diff_null
- differentiableAt_const_sub_iff
- differentiableAt_sub_const_iff
- differentiableOn_const_sub_iff
- differentiableOn_sub_const_iff
- differentiable_const_sub_iff
- differentiable_sub_const_iff
- directed_on_iUnion
- div_int_cast
- div_mem_center₀
- div_mod_eq_mod_mul_div
- div_nat_cast
- div_num_den
- div_rat_cast
- div_rat_cast_im
- drop_take_succ_eq_cons_get
- drop_take_succ_join_eq_get
- drop_take_succ_join_eq_get'
- drop_take_succ_join_eq_getElem
- dvd_div_iff
- empty'
- enumFrom_get?
- enum_get?
- eq
- eq_X_pow_of_natTrailingDegree_eq_natDegree
- eq_false_of_ne_true
- eq_false_or_eq_true
- eq_iff_eq_true_iff
- eq_int_castAddHom
- eq_of_eqv_lt
- eq_of_incomp
- eq_pow_of_mul_eq_pow_bit1
- eq_pow_of_mul_eq_pow_bit1_left
- eq_pow_of_mul_eq_pow_bit1_right
- eq_rpow_one_div_iff
- eq_true_of_ne_false
- equation_add'
- eqv_lt_iff_eq
- eraseIdx_insertNth
- eraseIdx_insertNth'
- erefl
- esymm
- etrans
- eval_int_cast
- eval_int_cast_map
- eval_nat_cast
- eval_nat_cast_map
- eval_nat_cast_mul
- eval_polynomial
- eval_polynomialX
- eval_polynomialX_zero
- eval_polynomialY
- eval_polynomialY_zero
- eval_polynomial_zero
- eval₂_at_int_cast
- eval₂_at_nat_cast
- eval₂_int_castRingHom_X
- eval₂_nat_cast
- ex_of_psig
- exists_continuous_snorm_sub_le_of_closed
- exists_intermediate_Set
- exists_intermediate_set
- exists_intermediate_set'
- exists_mem_forall_mem_nhds_within_pos
- exists_pos_set_lintegral_lt_of_measure_lt
- exists_snorm_indicator_le
- exists_subset_range_iff
- exists_unique_congr
- exists_unique_congr_left
- exists_unique_congr_left'
- expMapCircle
- expMapCircle_add
- expMapCircle_coe
- expMapCircle_neg
- expMapCircle_zero
- extractNth
- factorization_eq_factors_multiset
- factors
- factors_count_eq
- factors_eq_none_iff_zero
- find?_mem
- finset_sum_iSup_nat
- flip₁_continuous'
- flip₂_continuous'
- floor_coe
- floor_int_div_nat_eq_div
- floor_logb_nat_cast
- forall_congr_left'
- forgetAdjStar
- frange
- frange_ofSubring
- frange_one
- frange_zero
- frobenius_nat_cast
- fst_int_cast
- fst_nat_cast
- fullyFaithfulCancelRight
- fullyFaithfulCancelRight_hom_app
- fullyFaithfulCancelRight_inv_app
- fun_eq_funMulInvSnorm_mul_snorm
- germ_stalkSpecializes'
- germ_to_top
- get?_injective
- get?_length
- get?_zero_scanl
- get?_zip_with
- get?_zip_with_eq_some
- getD_replicate_default_eq
- getD_singleton_default_eq
- getElem?_zip_with
- getElem?_zip_with_eq_some
- getLast?_isNone
- getRest
- getString
- get_map_rev
- get_reverse
- get_set_of_ne
- get_splitWrtComposition
- get_splitWrtComposition'
- get_splitWrtCompositionAux
- get_zero_scanl
- get_zip
- get_zipWith
- ghostFun_int_cast
- ghostFun_nat_cast
- half_add_self
- has_deriv_at_interval_left_endpoint_of_tendsto_deriv
- has_deriv_at_interval_right_endpoint_of_tendsto_deriv
- has_fderiv_at_boundary_of_tendsto_fderiv
- iSup_coe_nat
- iSup_continuous
- iUnion
- iUnion_Icc_add_int_cast
- iUnion_Icc_int_cast
- iUnion_Ico_add_int_cast
- iUnion_Ico_int_cast
- iUnion_Ioc_add_int_cast
- iUnion_Ioc_int_cast
- iUnion_finset
- iUnion_null
- iUnion_null_iff
- id_continuous'
- id_eq
- incomp_iff_eq
- incomp_trans
- incomp_trans_of
- index_bot_eq_card
- inducedTopologyOfIsCoverDense
- inf_continuous
- inf_continuous'
- inf_eq_mul_of_coprime
- inf_le_left'
- inf_le_right'
- infty_coeFn_int_cast
- infty_coeFn_nat_cast
- inl_int_cast
- inl_nat_cast
- inner_indicatorConstLp_eq_inner_set_integral
- inner_indicatorConstLp_eq_set_integral_inner
- insertIdx_removeNth_of_le
- insertList
- insertNth_removeNth_of_ge
- instCommGroupOfExponentTwo
- instance (priority := 100) (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] :
- instance (priority := 100) isStrictTotalOrder_of_isStrictTotalOrder [IsStrictTotalOrder α r] :
- instance (priority := 100) isTotalPreorder_isPreorder (α : Sort u) (r : α → α → Prop)
- instance : IsTotalPreorder α (· ≤ ·)
- instance : LawfulMonad LazyList := LawfulMonad.mk'
- instance : LawfulTraversable LazyList := by
- instance : Traversable LazyList
- instance [LinearOrder α] : IsIncompTrans α (· < ·) := by infer_instance
- instance [LinearOrder α] : IsStrictWeakOrder α (· < ·) := by infer_instance
- instance [LinearOrder α] : IsTotalPreorder α (· ≤ ·)
- instance [LinearOrder α] : IsTotalPreorder α (· ≥ ·)
- intCast_smul
- int_apply
- int_cast_cast
- int_cast_coeff_zero
- int_cast_comp_cast
- int_cast_complex_norm
- int_cast_eq_int_cast_iff
- int_cast_eq_int_cast_iff'
- int_cast_eq_int_cast_iff_dvd_sub
- int_cast_fst
- int_cast_inj
- int_cast_mem_zmultiples_one
- int_cast_mod
- int_cast_mul_mem_zmultiples
- int_cast_ne
- int_cast_real_norm
- int_cast_rightInverse
- int_cast_snd
- int_cast_surjective
- int_cast_toProd
- int_cast_zmod_cast
- int_cast_zmod_eq_zero_iff_dvd
- int_coe_fst
- int_coe_ringEquivCongr
- int_coe_snd
- int_coe_zmod_eq_iff
- int_valuation_exists_uniformizer
- int_valuation_le_one
- int_valuation_le_pow_iff_dvd
- int_valuation_lt_one_iff_dvd
- int_valuation_ne_zero
- int_valuation_ne_zero'
- int_valuation_zero_le
- integrableOn_Ioc_of_interval_integral_norm_bounded
- integrableOn_Ioc_of_interval_integral_norm_bounded_left
- integrableOn_Ioc_of_interval_integral_norm_bounded_right
- integral_inner_eq_sq_snorm
- inter_sdiff
- inv_coe_int_den
- inv_coe_int_den_of_pos
- inv_coe_int_num
- inv_coe_int_num_of_pos
- inv_coe_nat_den
- inv_coe_nat_den_of_pos
- inv_coe_nat_num
- inv_coe_nat_num_of_pos
- inv_int_cast_smul_comm
- inv_int_cast_smul_eq
- inv_mem_center₀
- inv_nat_cast_smul_comm
- inv_nat_cast_smul_eq
- irrational_sqrt_rat_iff
- isAffineAffineScheme
- isAffineOfIso
- isAlpha
- isAlphanum
- isCaratheodory_iUnion_nat
- isClosed_setOf_continuous_of_le
- isDigit
- isEquiv
- isInt_cast
- isLUB_of_scottContinuous
- isLocalHomeomorph_expMapCircle
- isLower
- isNat_cast
- isNat_int_cast
- isNilpotent_of_finite_tFAE
- isNontrivial_iff
- isNontrivial_iff_ne_trivial
- isPrimitive
- isPrimitive.primitive_mul
- isSquare_zero
- isStrictWeakOrder_of_isTotalPreorder
- isStrictWeakOrder_of_linearOrder
- isUnit_den_of_num_eq_zero
- isUpper
- ite_continuous'
- iterate_derivative_X_pow_eq_nat_cast_mul
- iterate_derivative_int_cast_mul
- iterate_derivative_nat_cast_mul
- iterate_prod_map
- ker_int_castAddHom
- kernel
- keys
- leRecOn'
- le_coe_nat_sub
- le_eq_not_gt
- le_inter_add_diff
- le_multiplicity_iff_replicate_subperm_factors
- le_not_le_of_lt
- le_padicValNat_iff_replicate_subperm_factors
- le_snorm_of_bddBelow
- le_sup_left'
- le_sup_right'
- lift_nat_cast
- lintegral_le_of_forall_fin_meas_le'
- lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add
- lintegral_rpow_nnnorm_eq_rpow_snorm'
- lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top
- lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top
- lipschitzOn_univ
- listEquivLazyList
- log_int_cast_nonneg
- log_nat_cast_nonneg
- log_neg_nat_cast_nonneg
- lpMeas.ae_eq_zero_of_forall_set_integral_eq_zero
- lt_of_incomp_of_lt
- lt_of_lt_of_incomp
- lt_rpow_one_div_iff
- mapAdjunction
- map_add
- map_addY'
- map_add_mul
- map_coe_int
- map_coe_nat
- map_congr
- map_continuous'
- map_eq_set_lintegral_pdf
- map_filter
- map_hom_inv_app
- map_hom_inv_app_assoc
- map_int_cast
- map_inv_hom_app
- map_inv_hom_app_assoc
- map_inv_int_cast_smul
- map_inv_nat_cast_smul
- map_list_prod
- map_mul
- map_nat_cast
- map_nat_cast_smul
- map_neg_inv
- map_nsmul_pow
- map_one
- map_pow
- map_rat_cast_smul
- map_smul
- map_sum
- map_zero
- map_zero_one
- map_zsmul_zpow
- martingale_of_set_integral_eq_succ
- maximum_eq_none
- mdifferentiableAt_iff_liftPropAt
- mdifferentiableWithinAt_iff_liftPropWithinAt
- meas_ge_le_mul_pow_snorm
- meas_snormEssSup_lt
- mem_Lp_iff_snorm_lt_top
- mem_circle_iff_abs
- mem_circle_iff_normSq
- mem_frange_iff
- mem_posTangentConeAt_of_segment_subset'
- mem_primeFactors_iff_mem_factors
- memℒp_limitProcess_of_snorm_bdd
- minimum_eq_none
- mk_int_cast
- mono'
- mono_null
- monotone_sInf_of_monotone
- monotone_sSup_of_monotone
- mulSupport_int_cast
- mulSupport_nat_cast
- mul_X_add_nat_cast_comp
- mul_X_sub_int_cast_comp
- mul_div_mod_by_monic_cancel_left
- mul_div_mul_comm_of_dvd_dvd
- mul_eq_one_iff'
- mul_le_mul_of_le_of_le
- mul_lt_mul_of_le_of_le'
- mul_lt_mul_of_le_of_lt'
- mul_lt_mul_of_lt_of_lt'
- mul_lt_mul_of_pos_of_pos
- mul_meas_ge_le_pow_snorm
- mul_meas_ge_le_pow_snorm'
- mul_neg_eq_neg_mul_symm
- mul_num_den
- multinomial_nil
- natDegree_int_cast
- natDegree_int_cast_le
- natDegree_nat_cast
- natDegree_nat_cast_le
- natTrailingDegree_int_cast
- natTrailingDegree_nat_cast
- nat_apply
- nat_card_dvd_of_injective
- nat_card_dvd_of_le
- nat_card_dvd_of_surjective
- nat_cast_coeff_zero
- nat_cast_comp
- nat_cast_comp_val
- nat_cast_div
- nat_cast_dvd
- nat_cast_eq_iff
- nat_cast_eq_nat_cast_iff
- nat_cast_eq_nat_cast_iff'
- nat_cast_fst
- nat_cast_le
- nat_cast_le_ofReal
- nat_cast_le_toNNReal
- nat_cast_le_toNNReal'
- nat_cast_lt
- nat_cast_lt_ofReal
- nat_cast_lt_toNNReal
- nat_cast_mem_slitPlane
- nat_cast_mul_comp
- nat_cast_natAbs_norm
- nat_cast_natAbs_valMinAbs
- nat_cast_ne_zero
- nat_cast_nonneg
- nat_cast_pos
- nat_cast_rightInverse
- nat_cast_self'
- nat_cast_snd
- nat_cast_succ
- nat_cast_toNat
- nat_cast_toProd
- nat_cast_val
- nat_cast_zmod_eq_zero_iff_dvd
- nat_cast_zmod_surjective
- nat_cast_zmod_val
- nat_coe_fst
- nat_coe_snd
- nat_coe_zmod_eq_iff
- nat_ne_bot
- nat_succ_eq_int_succ
- neg_mul_eq_neg_mul_symm
- nil_asString_eq_empty
- noncommProd_map_aux
- noncommSum_map_aux
- nondegenerateRestrictOfDisjointOrthogonal
- nonsingular_add'
- norm_div_nat_cast
- norm_int_cast
- norm_int_cast_eq_padic_norm
- norm_nat_cast
- norm_set_integral_le_of_norm_le_const
- norm_set_integral_le_of_norm_le_const'
- norm_set_integral_le_of_norm_le_const_ae
- norm_set_integral_le_of_norm_le_const_ae'
- norm_set_integral_le_of_norm_le_const_ae''
- not_false'
- not_lt_of_equiv
- not_lt_of_equiv'
- not_ne
- not_not_iff
- not_summable_nat_cast_inv
- not_summable_one_div_nat_cast
- nsmul_eq_smul_cast
- ofFn_get_eq_map
- ofInt_eq_coe
- ofLazyList
- ofNat_eq_cast
- ofReal_coe_nat
- ofReal_eq_nat_cast
- ofReal_le_nat_cast
- ofReal_lt_nat_cast
- ofReal_rat_cast
- ofReal_set_integral_one
- ofReal_set_integral_one_of_measure_ne_top
- of_decide_iff
- of_int_cast
- of_iso
- of_iso_inv
- one_add_nat_cast
- one_eq_succ_zero
- pairwise_disjoint_Ico_add_int_cast
- pairwise_disjoint_Ico_int_cast
- pairwise_disjoint_Ioc_add_int_cast
- pairwise_disjoint_Ioc_int_cast
- pairwise_disjoint_Ioo_add_int_cast
- pairwise_disjoint_Ioo_int_cast
- permutations'Aux_get_zero
- polardCoord_symm_abs
- pos_of_subset_ne_zero
- pow_mul_meas_ge_le_snorm
- pow_ne_one_of_lt_orderOf'
- preimage_comp
- preimage_id
- preimage_map
- preservesCokernelsOfMapExact
- preservesKernelsOfMapExact
- prime_divisors_eq_to_filter_divisors_prime
- prime_divisors_filter_dvd_of_dvd
- primitiveCharFiniteField
- prod_of_empty
- prod_range_cast_nat_sub
- quadraticChar_isNontrivial
- rangeIsAffineOpenOfOpenImmersion
- range_half_space
- range_list_nthLe
- range_quadrant
- rat_cast_im
- rat_cast_imI
- rat_cast_imJ
- rat_cast_imK
- rat_cast_ne
- rat_cast_smul_eq
- rat_smul_mem
- relindex_bot_left_eq_card
- removeNth
- removeNth_eq_nthTail
- removeNth_insertNth'
- removeNth_val
- restrictNondegenerateOrthogonalSpanSingleton
- restrict_nondegenerate_of_isCompl_orthogonal
- ret
- riemannCompletedZeta
- riemannCompletedZeta_one_sub
- riemannCompletedZeta_residue_one
- riemannCompletedZeta₀
- riemannCompletedZeta₀_one_sub
- ringHom_eval₂_cast_int_ringHom
- rpow_one_div_eq_iff
- sFinite_withDensity_of_measurable
- sFinite_withDensity_of_sigmaFinite_of_measurable
- sSup_continuous
- sSup_continuous'
- sUnion_null_iff
- selfZPow_coe_nat
- selfZPow_neg_coe_nat
- selfZPow_sub_cast_nat
- self_cast_int_mul
- self_cast_int_mul_cast_int_mul
- self_cast_nat_mul
- self_cast_nat_mul_cast_nat_mul
- seq_compact_univ
- seq_continuous'
- setIntegral_condexpL1CLM
- set_integral_abs_condExp_le
- set_integral_abs_condexp_le
- set_integral_compLp
- set_integral_compProd_univ_left
- set_integral_compProd_univ_right
- set_integral_comp_smul
- set_integral_comp_smul_of_pos
- set_integral_condCDF
- set_integral_condExpInd
- set_integral_condExpIndSMul
- set_integral_condExpL1
- set_integral_condExpL1CLM
- set_integral_condExpL2_indicator
- set_integral_condexp
- set_integral_condexpInd
- set_integral_condexpIndSMul
- set_integral_condexpL1
- set_integral_condexpL1CLM
- set_integral_condexpL1CLM_of_measure_ne_top
- set_integral_condexpL2_indicator
- set_integral_congr
- set_integral_congr_ae
- set_integral_congr_ae₀
- set_integral_congr_set_ae
- set_integral_congr₀
- set_integral_density
- set_integral_densityProcess
- set_integral_densityProcess_of_le
- set_integral_densityProcess_of_mem
- set_integral_density_of_measurableSet
- set_integral_deterministic
- set_integral_deterministic'
- set_integral_dirac
- set_integral_dirac'
- set_integral_eq_integral_of_ae_compl_eq_zero
- set_integral_eq_integral_of_forall_compl_eq_zero
- set_integral_eq_of_subset_of_ae_diff_eq_zero
- set_integral_eq_of_subset_of_ae_diff_eq_zero_aux
- set_integral_eq_of_subset_of_forall_diff_eq_zero
- set_integral_eq_tsum
- set_integral_eq_tsum'
- set_integral_eq_zero_iff_of_nonneg_ae
- set_integral_eq_zero_of_ae_eq_zero
- set_integral_eq_zero_of_forall_eq_zero
- set_integral_ge_of_const_le
- set_integral_gt_gt
- set_integral_indicator
- set_integral_indicatorConstLp
- set_integral_le_integral
- set_integral_le_nonneg
- set_integral_map
- set_integral_map_equiv
- set_integral_mono
- set_integral_mono_ae
- set_integral_mono_ae_restrict
- set_integral_mono_on
- set_integral_mono_on_ae
- set_integral_mono_set
- set_integral_neg_eq_set_integral_nonpos
- set_integral_nonneg
- set_integral_nonneg_ae
- set_integral_nonneg_of_ae
- set_integral_nonneg_of_ae_restrict
- set_integral_nonpos
- set_integral_nonpos_ae
- set_integral_nonpos_le
- set_integral_nonpos_of_ae
- set_integral_nonpos_of_ae_restrict
- set_integral_piecewise
- set_integral_pos_iff_support_of_nonneg_ae
- set_integral_preCDF_fst
- set_integral_prod
- set_integral_prod_mul
- set_integral_re_add_im
- set_integral_restrict
- set_integral_stieltjesOfMeasurableRat
- set_integral_stieltjesOfMeasurableRat_rat
- set_integral_tilted
- set_integral_tilted'
- set_integral_toReal_rnDeriv
- set_integral_toReal_rnDeriv'
- set_integral_toReal_rnDeriv_eq_withDensity
- set_integral_toReal_rnDeriv_eq_withDensity'
- set_integral_toReal_rnDeriv_le
- set_integral_trim
- set_integral_withDensity_eq_set_integral_smul
- set_integral_withDensity_eq_set_integral_smul₀
- set_integral_withDensity_eq_set_integral_smul₀'
- set_lintegral_compProd_univ_left
- set_lintegral_compProd_univ_right
- set_lintegral_condCDF
- set_lintegral_condDistrib_of_measurableSet
- set_lintegral_congr
- set_lintegral_congr_fun
- set_lintegral_const_lt_top
- set_lintegral_density
- set_lintegral_deterministic
- set_lintegral_deterministic'
- set_lintegral_dirac
- set_lintegral_dirac'
- set_lintegral_empty
- set_lintegral_eq
- set_lintegral_eq_const
- set_lintegral_eq_tsum
- set_lintegral_eq_tsum'
- set_lintegral_le_lintegral
- set_lintegral_lt_top_of_bddAbove
- set_lintegral_lt_top_of_isCompact
- set_lintegral_map
- set_lintegral_max
- set_lintegral_measure_zero
- set_lintegral_mono
- set_lintegral_mono'
- set_lintegral_mono_ae
- set_lintegral_mono_ae'
- set_lintegral_nnnorm_condExpIndSMul_le
- set_lintegral_nnnorm_condExpL2_indicator_le
- set_lintegral_nnnorm_condexpIndSMul_le
- set_lintegral_nnnorm_condexpL2_indicator_le
- set_lintegral_one
- set_lintegral_pdf_le_map
- set_lintegral_piecewise
- set_lintegral_preCDF_fst
- set_lintegral_preimage_condDistrib
- set_lintegral_restrict
- set_lintegral_rnDeriv
- set_lintegral_rnDeriv'
- set_lintegral_rnDerivAux
- set_lintegral_rnDeriv_le
- set_lintegral_rnDeriv_mul
- set_lintegral_smul_measure
- set_lintegral_stieltjesOfMeasurableRat
- set_lintegral_stieltjesOfMeasurableRat_rat
- set_lintegral_strict_mono
- set_lintegral_subtype
- set_lintegral_tilted
- set_lintegral_tilted'
- set_lintegral_toKernel_Iic
- set_lintegral_toKernel_prod
- set_lintegral_toKernel_univ
- set_lintegral_univ
- set_lintegral_withDensity_eq_lintegral_mul₀
- set_lintegral_withDensity_eq_lintegral_mul₀'
- set_lintegral_withDensity_eq_set_lintegral_mul
- set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable
- set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀
- set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀'
- sets_iff_generate
- sign_coe_add_one
- sign_coe_nat_of_nonzero
- sign_int_cast
- sizeOf_dropSlice_lt
- slope_of_Xne
- slope_of_Yeq
- slope_of_Yne
- slope_of_Yne_eq_eval
- smeval_at_nat_cast
- smeval_nat_cast
- snd_int_cast
- snd_nat_cast
- snorm
- snorm'_add_le
- snorm'_add_le_of_le_one
- snorm'_congr_ae
- snorm'_congr_nnnorm_ae
- snorm'_congr_norm_ae
- snorm'_const
- snorm'_const'
- snorm'_const_of_isProbabilityMeasure
- snorm'_const_smul
- snorm'_const_smul_le
- snorm'_eq
- snorm'_eq_zero_iff
- snorm'_eq_zero_of_ae_zero
- snorm'_eq_zero_of_ae_zero'
- snorm'_exponent_zero
- snorm'_le_nnreal_smul_snorm'_of_ae_le_mul
- snorm'_le_snorm'_mul_rpow_measure_univ
- snorm'_le_snorm'_mul_snorm'
- snorm'_le_snorm'_of_exponent_le
- snorm'_le_snormEssSup
- snorm'_le_snormEssSup_mul_rpow_measure_univ
- snorm'_lim_eq_lintegral_liminf
- snorm'_lim_le_liminf_snorm'
- snorm'_lt_top_of_snorm'_lt_top_of_exponent_le
- snorm'_measure_zero_of_exponent_zero
- snorm'_measure_zero_of_neg
- snorm'_measure_zero_of_pos
- snorm'_mono_ae
- snorm'_mono_measure
- snorm'_mono_nnnorm_ae
- snorm'_neg
- snorm'_norm
- snorm'_norm_rpow
- snorm'_smul_le_mul_snorm'
- snorm'_smul_measure
- snorm'_sum_le
- snorm'_sum_norm_sub_le_tsum_of_cauchy_snorm'
- snorm'_trim
- snorm'_zero
- snorm'_zero'
- snormEssSup_add_le
- snormEssSup_congr_ae
- snormEssSup_const
- snormEssSup_const_smul
- snormEssSup_const_smul_le
- snormEssSup_eq_zero_iff
- snormEssSup_indicator_const_eq
- snormEssSup_indicator_const_le
- snormEssSup_indicator_eq_snormEssSup_restrict
- snormEssSup_indicator_le
- snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul
- snormEssSup_le_of_ae_bound
- snormEssSup_le_of_ae_nnnorm_bound
- snormEssSup_lt_top_of_ae_bound
- snormEssSup_lt_top_of_ae_nnnorm_bound
- snormEssSup_map_measure
- snormEssSup_measure_zero
- snormEssSup_mono_measure
- snormEssSup_mono_nnnorm_ae
- snormEssSup_piecewise
- snormEssSup_smul_measure
- snormEssSup_trim
- snormEssSup_zero
- snorm_add_le
- snorm_add_le'
- snorm_add_lt_top
- snorm_aeeqFun
- snorm_comp_measurePreserving
- snorm_condExpL2_le
- snorm_condexpL2_le
- snorm_congr_ae
- snorm_congr_nnnorm_ae
- snorm_congr_norm_ae
- snorm_const
- snorm_const'
- snorm_const_lt_top_iff
- snorm_const_smul
- snorm_const_smul_le
- snorm_densityProcess_le
- snorm_density_le
- snorm_eq
- snorm_eq_lintegral_rpow_nnnorm
- snorm_eq_snorm'
- snorm_eq_zero_and_zero_of_ae_le_mul_neg
- snorm_eq_zero_iff
- snorm_exponent_top
- snorm_exponent_top_lim_eq_essSup_liminf
- snorm_exponent_top_lim_le_liminf_snorm_exponent_top
- snorm_exponent_zero
- snorm_indicator_const
- snorm_indicator_const'
- snorm_indicator_const_le
- snorm_indicator_const₀
- snorm_indicator_eq_restrict
- snorm_indicator_eq_snorm_restrict
- snorm_indicator_ge_of_bdd_below
- snorm_indicator_le
- snorm_indicator_le_of_bound
- snorm_indicator_sub_indicator
- snorm_inner_lt_top
- snorm_le_add_measure_left
- snorm_le_add_measure_right
- snorm_le_mul_snorm_of_ae_le_mul
- snorm_le_nnreal_smul_snorm_of_ae_le_mul
- snorm_le_of_ae_bound
- snorm_le_of_ae_nnnorm_bound
- snorm_le_snorm_fderiv
- snorm_le_snorm_fderiv_of_eq
- snorm_le_snorm_fderiv_of_eq_inner
- snorm_le_snorm_fderiv_of_le
- snorm_le_snorm_fderiv_one
- snorm_le_snorm_mul_rpow_measure_univ
- snorm_le_snorm_mul_snorm'_of_norm
- snorm_le_snorm_mul_snorm_of_nnnorm
- snorm_le_snorm_mul_snorm_top
- snorm_le_snorm_of_exponent_le
- snorm_le_snorm_top_mul_snorm
- snorm_lim_le_liminf_snorm
- snorm_lt_top
- snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top
- snorm_map_measure
- snorm_measure_zero
- snorm_mono
- snorm_mono_ae
- snorm_mono_ae_real
- snorm_mono_measure
- snorm_mono_nnnorm
- snorm_mono_nnnorm_ae
- snorm_mono_real
- snorm_ne_top
- snorm_neg
- snorm_nnreal_eq_lintegral
- snorm_nnreal_eq_snorm'
- snorm_nnreal_pow_eq_lintegral
- snorm_norm
- snorm_norm_rpow
- snorm_one_add_measure
- snorm_one_condExp_le_snorm
- snorm_one_condexp_le_snorm
- snorm_one_eq_lintegral_nnnorm
- snorm_one_le_of_le
- snorm_one_le_of_le'
- snorm_one_smul_measure
- snorm_restrict_eq_of_support_subset
- snorm_restrict_le
- snorm_rpow_two_norm_lt_top
- snorm_smul_le_mul_snorm
- snorm_smul_le_snorm_mul_snorm_top
- snorm_smul_le_snorm_top_mul_snorm
- snorm_smul_measure_of_ne_top
- snorm_smul_measure_of_ne_zero
- snorm_smul_measure_of_ne_zero_of_ne_top
- snorm_sub_le
- snorm_sub_le'
- snorm_sub_le_of_dist_bdd
- snorm_sum_le
- snorm_top_piecewise
- snorm_trim
- snorm_trim_ae
- snorm_zero
- snorm_zero'
- some_add_self_of_Yeq
- some_add_self_of_Yne
- some_add_self_of_Yne'
- some_add_some_of_Xne
- some_add_some_of_Xne'
- some_add_some_of_Yeq
- some_add_some_of_Yne
- some_add_some_of_Yne'
- squarefree_coe_nat
- squarefree_iff_nodup_factors
- stalkMap_germ'
- stalkMap_germ'_assoc
- star
- star_int_cast_smul
- star_inv_int_cast_smul
- star_inv_nat_cast_smul
- star_nat_cast_smul
- star_rat_cast_smul
- subInduction
- sublist_of_cons_sublist_cons
- submartingale_of_set_integral_le
- submartingale_of_set_integral_le_succ
- subset_starSubalgebra
- subtype_of_exists
- succAbove_lt_ge
- succAbove_lt_gt
- succ_coe_nat_pos
- succ_neg_nat_succ
- sum_count_eq
- sup_continuous
- sup_natCast
- sup_nat_cast
- supermartingale_of_set_integral_succ_le
- support_int_cast
- support_nat_cast
- symm_castIso
- tailing
- tailingLinearEquiv
- tailing_disjoint_tunnel_succ
- tailing_le_tunnel
- tailing_sup_tunnel_succ_le_tunnel
- tailings
- tailings_disjoint_tailing
- tailings_disjoint_tunnel
- tailings_succ
- tailings_zero
- tendstoInMeasure_of_tendsto_snorm
- tendstoInMeasure_of_tendsto_snorm_of_ne_top
- tendstoInMeasure_of_tendsto_snorm_of_stronglyMeasurable
- tendstoInMeasure_of_tendsto_snorm_top
- tendsto_approxOn_Lp_snorm
- tendsto_approxOn_range_Lp_snorm
- tendsto_int_cast_atBot_iff
- tendsto_int_cast_atTop_atTop
- tendsto_int_cast_atTop_iff
- tendsto_nat_cast_atTop_atTop
- tendsto_nat_cast_atTop_iff
- tendsto_rat_cast_atBot_iff
- tendsto_rat_cast_atTop_iff
- tendsto_removeNth
- tendsto_set_integral_densityProcess
- tendsto_set_integral_of_L1
- tendsto_set_integral_of_L1'
- tendsto_set_integral_of_antitone
- tendsto_set_integral_of_monotone
- tendsto_set_lintegral_zero
- tendsto_snorm_condExp
- tendsto_snorm_condexp
- tendsto_snorm_one_densityProcess_limitProcess
- tendsto_snorm_one_restrict_densityProcess_limitProcess
- toEnd_int_cast
- toEnd_nat_cast
- toFinsupp_cons_apply_succ
- toFinsupp_cons_apply_zero
- toLazyList
- toLin'_apply
- toLinHom
- toLinHomAux₂
- toList_inv_asString
- toNNReal_eq_nat_cast
- toNNReal_le_nat_cast
- toNNReal_lt_nat_cast
- toNNReal_lt_nat_cast'
- toNat_coe_nat
- toNat_coe_nat_add_one
- toOption_isNone
- topIsAffineOpen
- top_continuous
- totallyBounded_subset
- trace_comp_toEnd_weight_space_eq
- transferNatTrans
- transferNatTransSelf
- truncateFun_int_cast
- truncateFun_nat_cast
- tunnel
- tunnel'
- tunnelAux
- tunnelAux_injective
- union
- union_null
- units_eq_one
- universallyIsLocalAtTarget
- universallyIsLocalAtTargetOfMorphismRestrict
- val_int_cast
- val_nat_cast_of_lt
- values
- zpow_eq_zero
- zpow_ne_zero_of_ne_zero
- zpow_neg_coe_nat
- zsmul_eq_smul_cast
- ΓSpec.adjunction_unit_app_app_top
- ΓSpec.adjunction_unit_map_basicOpen
- ΓSpec.adjunction_unit_naturality
- ΓSpec.adjunction_unit_naturality_assoc
- ⟨ne_of_val_ne,
-- IsNontrivial
-- _
-- cast_int_mul_cast_int_mul
-- cast_int_mul_left
-- cast_int_mul_right
-- coe_int
-- coe_nat_div
-- coe_rat_cast
-- continuous_removeNth
-- exists_smaller_set
-- int_cast_apply
-- int_cast_def
-- int_cast_im
-- int_cast_imI
-- int_cast_imJ
-- int_cast_imK
-- int_cast_re
-- le_rpow_one_div_iff
-- map_neg
-- map_sub
-- mk_coe_nat
-- mk_nat_cast
-- mul_eq_one_iff
-- nat_cast_apply
-- nat_cast_def
-- nat_cast_eq_zero
-- nat_cast_im
-- nat_cast_imI
-- nat_cast_imJ
-- nat_cast_imK
-- nat_cast_inj
-- nat_cast_mod
-- nat_cast_mul
-- nat_cast_re
-- nat_cast_self
-- nat_cast_sub
-- nat_ne_top
-- nnnorm_coe_nat
-- noncommProd_map
-- noncommSum_map
-- normSq_int_cast
-- normSq_nat_cast
-- normSq_rat_cast
-- norm_coe_nat
-- null_of_locally_null
-- of_nat_cast
-- removeNth_insertNth
-- rpow_int_cast
-- rpow_one_div_le_iff
-- set_integral_compProd
-- set_integral_condKernel
-- set_integral_condKernel_univ_left
-- set_integral_condKernel_univ_right
-- set_integral_const
-- set_integral_eq
-- set_integral_le
-- set_lintegral_compProd
-- set_lintegral_condKernel
-- set_lintegral_condKernel_eq_measure_prod
-- set_lintegral_condKernel_univ_left
-- set_lintegral_condKernel_univ_right
-- set_lintegral_const
-- smul_one_eq_coe
-- stalkToFiberRingHom_germ'
-- sum_of_empty
-- top_ne_nat
-- val_nat_cast
--- coe_nat_mem
--- int_cast
--- nat_cast
--- rpow_nat_cast
---- coe_int_mem
------ coe_nat
------- coe_int_cast
--------- coe_nat_cast

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.

Decrease in tech debt: (relative, absolute) = (9.06, 1.13)

Current number	Change	Type
4263	-1	porting notes
1406	-1	erw
88	-13	disabled deprecation lints
50	-2	large files
11	-4	`Deprecated` files
771	-444	total LoC in `Deprecated` files

Current commit b8844fc5d8
Reference commit 74bf56fd21

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

Mathlib/Deprecated/Aliases.lean

kim-em · 2025-01-31T22:50:06Z

bors d+

mathlib-bors · 2025-01-31T22:50:08Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

erdOne · 2025-01-31T23:37:55Z

Mathlib/Algebra/Algebra/Equiv.lean

-section map
-
-@[deprecated map_add (since := "2024-06-20")]
-protected theorem map_add : ∀ x y, e (x + y) = e x + e y :=
-  map_add e
-
-@[deprecated map_zero (since := "2024-06-20")]
-protected theorem map_zero : e 0 = 0 :=
-  map_zero e
-
-@[deprecated map_mul (since := "2024-06-20")]
-protected theorem map_mul : ∀ x y, e (x * y) = e x * e y :=
-  map_mul e
-
-@[deprecated map_one (since := "2024-06-20")]
-protected theorem map_one : e 1 = 1 :=
-  map_one e
-
-@[deprecated map_smul (since := "2024-06-20")]
-protected theorem map_smul (r : R) (x : A₁) : e (r • x) = r • e x :=
-  map_smul _ _ _
-
-@[deprecated map_pow (since := "2024-06-20")]
-protected theorem map_pow : ∀ (x : A₁) (n : ℕ), e (x ^ n) = e x ^ n :=
-  map_pow _
-
-end map
-


I thought the plan was to un-deprecate these instead of removing them?

Do you want to do that now? It's been seven months since they were deprecated

I've reverted, but please consider acting soon

ghost · 2025-02-01T07:52:23Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors · 2025-02-01T08:08:06Z

Merge conflict.

…?(protected )?alias[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n?

ghost · 2025-02-01T09:03:19Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

…1271) The first commit was done by replacing all matches of `@\[deprecated.*\(since := "2024-0[1-7]-.."\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n?` with nothing. The second commit was done manually.

mathlib-bors · 2025-02-01T09:16:33Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

…1271) The first commit was done by replacing all matches of `@\[deprecated.*\(since := "2024-0[1-7]-.."\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n?` with nothing. The second commit was done manually.

The first commit was done automatically using #21271's method, with the regex ``` @\[deprecated.*\(since := "2024-10-([01].|2[01])"\)\][\s\n]?(protected )?alias [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n? ``` The remaining commits are manual removals of empty sections and missed deprecations (`2024-10-([01].|2[01])`).

YaelDillies added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 30, 2025

gio256 reviewed Jan 30, 2025

View reviewed changes

Mathlib/Deprecated/Aliases.lean Show resolved Hide resolved

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2025

YaelDillies force-pushed the delete_deprecations_2024_jan_to_jul branch from 781dd47 to 1676052 Compare January 31, 2025 08:07

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 31, 2025

gio256 mentioned this pull request Jan 31, 2025

chore: remove deprecations from 2024-04 #21242

Closed

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 31, 2025

erdOne reviewed Jan 31, 2025

View reviewed changes

YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 1, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Feb 1, 2025

YaelDillies added 3 commits February 1, 2025 08:12

@\[deprecated.*\(since := "2024-0[1-7]-.."\)\][\s\n]?(noncomputable )…

b674dc6

…?(protected )?alias[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]* :=[\s\n]+[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟'.₀₁₂₃₄₅₆₇₈₉]*\n\n?

manual

2d89d97

revert

b8844fc

YaelDillies force-pushed the delete_deprecations_2024_jan_to_jul branch from e07d2f6 to b8844fc Compare February 1, 2025 08:12

mathlib-bors bot changed the title ~~chore: delete declarations deprecated between 2024-01 and 2024-07~~ [Merged by Bors] - chore: delete declarations deprecated between 2024-01 and 2024-07 Feb 1, 2025

mathlib-bors bot closed this Feb 1, 2025

mathlib-bors bot deleted the delete_deprecations_2024_jan_to_jul branch February 1, 2025 09:16

YaelDillies mentioned this pull request Apr 21, 2025

chore: delete >6 month old deprecations (2024-10 11-20) #24238

Closed

Parcly-Taxel mentioned this pull request Apr 22, 2025

[Merged by Bors] - chore: delete >6 month old deprecations (2024-10 11-21) #24271

Closed

bryangingechen mentioned this pull request Sep 4, 2025

feat: automation for removing outdated deprecations #27956

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: delete declarations deprecated between 2024-01 and 2024-07#21271

[Merged by Bors] - chore: delete declarations deprecated between 2024-01 and 2024-07#21271
YaelDillies wants to merge 3 commits intomasterfrom
delete_deprecations_2024_jan_to_jul

YaelDillies commented Jan 30, 2025

Uh oh!

github-actions bot commented Jan 30, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

kim-em commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

erdOne Jan 31, 2025

Uh oh!

YaelDillies Feb 1, 2025

Uh oh!

YaelDillies Feb 1, 2025

Uh oh!

ghost commented Feb 1, 2025

Uh oh!

mathlib-bors bot commented Feb 1, 2025

Uh oh!

ghost commented Feb 1, 2025

Uh oh!

mathlib-bors bot commented Feb 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

YaelDillies commented Jan 30, 2025

Uh oh!

github-actions bot commented Jan 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b8844fc5d8

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

kim-em commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

erdOne Jan 31, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 1, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 1, 2025

Choose a reason for hiding this comment

Uh oh!

ghost commented Feb 1, 2025

Uh oh!

mathlib-bors bot commented Feb 1, 2025

Uh oh!

ghost commented Feb 1, 2025

Uh oh!

mathlib-bors bot commented Feb 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Jan 30, 2025 •

edited

Loading