[Merged by Bors] - chore(Data/Complex): deprecate Complex.abs
#21995
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
PR summary f023af284c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Complex.Abs | 1196 | 0 | -1196 (-100.00%) |
| Mathlib.Analysis.Complex.Basic | 1488 | 1482 | -6 (-0.40%) |
| Mathlib.Analysis.Complex.AbelLimit | 1548 | 1544 | -4 (-0.26%) |
| Mathlib.NumberTheory.Modular | 1745 | 1741 | -4 (-0.23%) |
| Mathlib.Data.Complex.Order | 1197 | 1199 | +2 (+0.17%) |
| Mathlib.Analysis.SpecialFunctions.Exponential | 1669 | 1667 | -2 (-0.12%) |
| Mathlib.Data.Complex.Norm | 1199 | 1198 | -1 (-0.08%) |
| Mathlib.Data.Complex.Exponential | 1219 | 1218 | -1 (-0.08%) |
| Mathlib.Data.Complex.Trigonometric | 1220 | 1219 | -1 (-0.08%) |
| Mathlib.Analysis.SpecialFunctions.Exp | 1547 | 1546 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.Circle | 1550 | 1549 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.UnitDisc.Basic | 1552 | 1551 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | 1558 | 1557 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Arg | 1612 | 1611 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Log | 1615 | 1614 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Pow.Real | 1617 | 1616 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Circle | 1619 | 1618 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics | 1619 | 1618 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Pow.Continuity | 1620 | 1619 | -1 (-0.06%) |
| Mathlib.Analysis.PSeries | 1622 | 1621 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.CompareExp | 1624 | 1623 | -1 (-0.06%) |
| Mathlib.RingTheory.RootsOfUnity.Complex | 1654 | 1653 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.Arg | 1659 | 1658 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.Series | 1670 | 1669 | -1 (-0.06%) |
| Mathlib.MeasureTheory.Function.SpecialFunctions.Basic | 1670 | 1669 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.Isometry | 1741 | 1740 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv | 1777 | 1776 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv | 1779 | 1778 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Pow.Deriv | 1793 | 1792 | -1 (-0.06%) |
| Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence | 1824 | 1823 | -1 (-0.05%) |
| Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty | 1829 | 1828 | -1 (-0.05%) |
| Mathlib.Analysis.PSeriesComplex | 1834 | 1833 | -1 (-0.05%) |
| Mathlib.NumberTheory.LSeries.Basic | 1834 | 1833 | -1 (-0.05%) |
| Mathlib.NumberTheory.LSeries.Injectivity | 1841 | 1840 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Angle | 1849 | 1848 | -1 (-0.05%) |
| Mathlib.Analysis.InnerProductSpace.TwoDim | 1886 | 1885 | -1 (-0.05%) |
| Mathlib.Geometry.Euclidean.Angle.Oriented.Basic | 1888 | 1887 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Metric | 1897 | 1896 | -1 (-0.05%) |
| Mathlib.Probability.Moments.IntegrableExpMul | 1926 | 1925 | -1 (-0.05%) |
| Mathlib.RingTheory.Polynomial.Cyclotomic.Eval | 1975 | 1974 | -1 (-0.05%) |
| Mathlib.MeasureTheory.Integral.CircleIntegral | 2107 | 2106 | -1 (-0.05%) |
| Mathlib.MeasureTheory.Integral.CircleTransform | 2108 | 2107 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Integrals | 2123 | 2122 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Complex.LogBounds | 2127 | 2126 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Arctan | 2128 | 2127 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Log.Summable | 2129 | 2128 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.PolarCoord | 2132 | 2131 | -1 (-0.05%) |
| Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart | 2132 | 2131 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.CauchyIntegral | 2146 | 2145 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Liouville | 2147 | 2146 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Positivity | 2148 | 2147 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.LocallyUniformLimit | 2151 | 2150 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Periodic | 2153 | 2152 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.AbsMax | 2155 | 2154 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.PhragmenLindelof | 2157 | 2156 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Schwarz | 2158 | 2157 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.OpenMapping | 2159 | 2158 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.Hadamard | 2168 | 2167 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.ImproperIntegrals | 2169 | 2168 | -1 (-0.05%) |
| Mathlib.Analysis.Fourier.AddCircle | 2171 | 2170 | -1 (-0.05%) |
| Mathlib.Analysis.MellinTransform | 2171 | 2170 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Gamma.Basic | 2172 | 2171 | -1 (-0.05%) |
| Mathlib.Analysis.Fourier.AddCircleMulti | 2174 | 2173 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Gamma.Deriv | 2175 | 2174 | -1 (-0.05%) |
| Mathlib.MeasureTheory.Integral.Gamma | 2175 | 2174 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral | 2179 | 2178 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Exp | 2180 | 2179 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent | 2181 | 2180 | -1 (-0.05%) |
| Mathlib.Probability.Moments.ComplexMGF | 2182 | 2181 | -1 (-0.05%) |
| Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls | 2191 | 2190 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform | 2211 | 2210 | -1 (-0.05%) |
| Mathlib.Analysis.Fourier.Inversion | 2213 | 2212 | -1 (-0.05%) |
| Mathlib.Analysis.SpecialFunctions.Gamma.Beta | 2214 | 2213 | -1 (-0.05%) |
| Mathlib.NumberTheory.LSeries.MellinEqDirichlet | 2216 | 2215 | -1 (-0.05%) |
| Mathlib.NumberTheory.ModularForms.QExpansion | 2225 | 2224 | -1 (-0.04%) |
| Mathlib.NumberTheory.ZetaValues | 2225 | 2224 | -1 (-0.04%) |
| Mathlib.Analysis.Fourier.FourierTransformDeriv | 2228 | 2227 | -1 (-0.04%) |
| Mathlib.NumberTheory.ModularForms.LevelOne | 2237 | 2236 | -1 (-0.04%) |
| Mathlib.Analysis.CStarAlgebra.Spectrum | 2279 | 2278 | -1 (-0.04%) |
| Mathlib.Analysis.Fourier.PoissonSummation | 2288 | 2287 | -1 (-0.04%) |
| Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation | 2289 | 2288 | -1 (-0.04%) |
| Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable | 2295 | 2294 | -1 (-0.04%) |
| Mathlib.NumberTheory.LSeries.HurwitzZetaEven | 2310 | 2309 | -1 (-0.04%) |
| Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable | 2310 | 2309 | -1 (-0.04%) |
| Mathlib.NumberTheory.LSeries.RiemannZeta | 2314 | 2313 | -1 (-0.04%) |
| Mathlib.NumberTheory.NumberField.Embeddings | 2328 | 2327 | -1 (-0.04%) |
| Mathlib.NumberTheory.LSeries.Dirichlet | 2386 | 2385 | -1 (-0.04%) |
| Mathlib.NumberTheory.EulerProduct.DirichletLSeries | 2389 | 2388 | -1 (-0.04%) |
| Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic | 2536 | 2535 | -1 (-0.04%) |
| Mathlib.NumberTheory.NumberField.House | 2543 | 2542 | -1 (-0.04%) |
| Mathlib.NumberTheory.LSeries.ZMod | 2547 | 2546 | -1 (-0.04%) |
| Mathlib.NumberTheory.LSeries.Nonvanishing | 2571 | 2570 | -1 (-0.04%) |
| Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody | 2603 | 2602 | -1 (-0.04%) |
| Mathlib.NumberTheory.NumberField.Discriminant.Basic | 2617 | 2616 | -1 (-0.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.Complex.Abs |
-1196 |
13 filesMathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Convex.Strong Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Topology.ContinuousMap.StarOrdered |
-6 |
54 filesMathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Continuous Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Measure.Complex Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.NumberTheory.Modular Mathlib.Topology.Instances.Complex |
-4 |
3 filesMathlib.Analysis.SpecialFunctions.Exponential Mathlib.Combinatorics.Derangements.Exponential Mathlib.Probability.Distributions.Poisson |
-2 |
511 filesMathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Isometry Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.Matrix Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Normed.Algebra.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.Normed.Ring.SmoothingSeminorm Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.SpecialFunctions.Arsinh 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.CircleAddChar Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Exp 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.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq Mathlib.Analysis.SpecialFunctions.NonIntegrable 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.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.FloorPow Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Data.Complex.ExponentialBounds Mathlib.Data.Complex.Exponential Mathlib.Data.Complex.Norm Mathlib.Data.Complex.Trigonometric Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Real.Pi.Irrational Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj 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.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.LDL Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedLebesgue 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.ConvergenceInMeasure 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.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.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic 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.BochnerL1 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.MeanInequalities 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.Doubling 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.NumberTheory.AbelSummation Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence 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.MulChar.Lemmas Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.WellApproximable Mathlib.NumberTheory.ZetaValues 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.AbsolutelyContinuous 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.RingTheory.LittleWedderburn Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski |
-1 |
Mathlib.Data.Complex.Order |
2 |
Declarations diff
+ Function.Periodic.im_invQParam_pos_of_norm_lt_one
+ Function.Periodic.norm_qParam_le_of_one_half_le_im
+ UpperHalfPlane.norm_exp_two_pi_I_lt_one
+ UpperHalfPlane.norm_qParam_lt_one
+ abs
+ abs_im_div_norm_le_one
+ abs_im_eq_norm
+ abs_im_le_norm
+ abs_im_lt_norm
+ abs_re_div_norm_le_one
+ abs_re_eq_norm
+ abs_re_le_norm
+ abs_re_lt_norm
+ basis_repr_norm_le_const_mul_house
+ cauSeqNorm
+ continuousOn_norm_circleTransformBoundingFunction
+ ext_norm_arg
+ ext_norm_arg_iff
+ im_le_norm
+ instNorm
+ isAbsoluteValueNorm
+ isCauSeq_norm
+ isCauSeq_norm_exp
+ isLittleO_log_norm_re
+ lim_norm
+ neg_re_eq_norm
+ norm_add_eq
+ norm_add_eq_iff
+ norm_add_mul_I
+ norm_circleMap_zero
+ norm_circleTransformBoundingFunction_le
+ norm_coe
+ norm_complexMGF_le_mgf
+ norm_conj
+ norm_cos_add_sin_mul_I
+ norm_cpow_eq_rpow_re_of_nonneg
+ norm_cpow_eq_rpow_re_of_pos
+ norm_cpow_inv_nat
+ norm_cpow_le
+ norm_cpow_of_imp
+ norm_cpow_of_ne_zero
+ norm_cpow_real
+ norm_def
+ norm_deriv_le_one_of_mapsTo_ball
+ norm_div
+ norm_eq_one_iff
+ norm_eq_one_iff'
+ norm_eq_sqrt_sq_add_sq
+ norm_exp
+ norm_exp_eq_iff_re_eq
+ norm_exp_le_exp_norm
+ norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le
+ norm_exp_ofReal
+ norm_exp_sub_one_le
+ norm_exp_sub_one_sub_id_le
+ norm_exp_sub_sum_le_exp_norm_sub_sum
+ norm_exp_sub_sum_le_norm_mul_exp
+ norm_invInterpStrip
+ norm_le_abs_re_add_abs_im
+ norm_le_norm_of_mapsTo_ball_self
+ norm_le_sqrt_two_mul_max
+ norm_le_tsum_norm
+ norm_lt_one
+ norm_mul
+ norm_mul_cos_add_sin_mul_I
+ norm_mul_cos_arg
+ norm_mul_exp_arg_mul_I
+ norm_mul_self_eq_normSq
+ norm_mul_sin_arg
+ norm_ne_one
+ norm_of_nonneg
+ norm_polarCoord_symm
+ norm_pow
+ norm_prod
+ norm_qParam
+ norm_qParam_lt_iff
+ norm_sub_eq
+ norm_sub_eq_iff
+ norm_two
+ norm_zpow
+ range_norm
+ re_eq_neg_norm
+ re_eq_norm
+ re_le_norm
+ sq_norm
+ sq_norm_sub_sq_im
+ sq_norm_sub_sq_re
+ tendsto_norm
+ tendsto_norm_tan_atTop
+ tendsto_norm_tan_of_cos_eq_zero
+-- abs_conj
- _root_.Complex.abs
- abs_def
- instance : Norm ℂ
- norm_eq_abs
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) = (6.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 3360 | -6 | porting notes |
Current commit f023af284c
Reference commit db136357e9
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
leanprover-community-bot-assistant
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
vihdzp
reviewed
Feb 20, 2025
| (sameRay_of_arg_eq h).norm_sub | ||
|
|
||
| @[deprecated (since := "2025-02-17")] alias abs_add_eq_iff := norm_add_eq_iff |
There was a problem hiding this comment.
I think in situations like these we like keeping the deprecated lemmas written exactly the same as they were before deprecation. I can see how this gets ugly here, so maybe someone else can chime in with an opinion.
There was a problem hiding this comment.
The problem here is that I cannot keep the original statement since Complex.abs is now deprecated: it would trigger a warning.
|
Thanks 🎉 bors merge |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 24, 2025
in this PR: - Defines `Complex.norm` directly - Defines `Complex.abs` as `Complex.norm` and deprecate it - Change `Complex.abs` to `norm` in all definitions / statements / proofs - Delete `Complex.norm_eq_abs` and the file `Data.Complex.Abs` (its results are moved as deprecated aliases in `Data.Complex.Norm`) - Change the name of all results which refer to `Complex.abs` to use `norm` instead and deprecate the original names Co-authored-by: Xavier Roblot <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Complex.absComplex.abs
Julian
added a commit
that referenced
this pull request
Feb 24, 2025
* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)
Champitoad
pushed a commit
that referenced
this pull request
Feb 25, 2025
in this PR: - Defines `Complex.norm` directly - Defines `Complex.abs` as `Complex.norm` and deprecate it - Change `Complex.abs` to `norm` in all definitions / statements / proofs - Delete `Complex.norm_eq_abs` and the file `Data.Complex.Abs` (its results are moved as deprecated aliases in `Data.Complex.Norm`) - Change the name of all results which refer to `Complex.abs` to use `norm` instead and deprecate the original names Co-authored-by: Xavier Roblot <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
in this PR:
Complex.normdirectlyComplex.absasComplex.normand deprecate itComplex.abstonormin all definitions / statements / proofsComplex.norm_eq_absand the fileData.Complex.Abs(its results are moved as deprecated aliases inData.Complex.Norm)Complex.absto usenorminstead and deprecate the original names