[Merged by Bors] - feat: lemmas about forgetting linearity of ContinuousLinearMap by eric-wieser · Pull Request #21444 · leanprover-community/mathlib4

eric-wieser · 2025-02-05T00:03:22Z

depends on: [Merged by Bors] - chore(Topology/Algebra/ContinuousMonoidHom): do not depend on ContinuousLinearMap #21443

…uousLinearMap` The dependency should go in the other direction.

github-actions · 2025-02-05T00:04:16Z

PR summary 3092a7c8f5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.Module.LinearMap	1118	1119	+1 (+0.09%)

Import changes for all files

Files	Import difference
918 files `Mathlib.Algebra.Order.AbsoluteValue.Equivalence` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `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.OfScalars` `Mathlib.Analysis.Analytic.Order` `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.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `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.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.CStarAlgebra.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.InnerProduct` `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.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.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `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.Body` `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.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.Normed` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `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.JointEigenspace` `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.Semisimple` `Mathlib.Analysis.InnerProductSpace.Spectrum` `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.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Order` `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.Connected` `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.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.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `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.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.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `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.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `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.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `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.VonNeumannAlgebra.Basic` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.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.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.ExponentialBounds` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `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.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.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.Transform` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.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.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `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.LinearAlgebra.QuadraticForm.Real` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `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.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.L1Space.AEEqFun` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `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.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.MeasureTheory.Function.LpSpace` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `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.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `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.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `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.MeasureTheory.VectorMeasure.WithDensity` `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.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `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.PrimesCongruentOne` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Integrable` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Integration` `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.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Integral` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.Probability.Kernel.Proper` `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.IntegrableExpMul` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.UniformOn` `Mathlib.Probability.Variance` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.Perfection` `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.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.ContinuousAffineMap` `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.CharacterSpace` `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.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `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.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.Baire.BaireMeasurable` `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.Nobeling` `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.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.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.Germ` `Mathlib.Topology.Instances.Complex` `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.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.TietzeExtension` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom`	1

Declarations diff

+ coe_one
+ instance : CommMonoid (ContinuousMonoidHom A E)
+ instance : Inhabited (ContinuousMonoidHom A B) := ⟨1⟩
+ instance : One (ContinuousMonoidHom A B)
+ toContinuousAddMonoidHom_add
+ toContinuousAddMonoidHom_comp
+ toContinuousAddMonoidHom_id
+ toContinuousAddMonoidHom_inj
+ toContinuousAddMonoidHom_injective
+ toContinuousAddMonoidHom_neg
+ toContinuousAddMonoidHom_restrictScalars
+ toContinuousAddMonoidHom_sub
+ toContinuousAddMonoidHom_zero
- instance : Inhabited (ContinuousMonoidHom A B)
- one

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

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

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

mathlib4-dependent-issues-bot · 2025-02-05T09:46:40Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Topology/Algebra/ContinuousMonoidHom): do not depend on ContinuousLinearMap #21443~~
By Dependent Issues (🤖). Happy coding!

jcommelin

Thanks 🎉

bors merge

Co-authored-by: Eric Wieser <efw@google.com>

mathlib-bors · 2025-02-11T17:01:24Z

Pull request successfully merged into master.

Build succeeded:

eric-wieser added 4 commits February 4, 2025 22:52

chore(Topology/Algebra/ContinuousMonoidHom): do not depend on `Contin…

289342f

…uousLinearMap` The dependency should go in the other direction.

missing file

1ef0744

wip

3d3a701

lots of helper lemmas

a4023e0

github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Feb 5, 2025

eric-wieser mentioned this pull request Feb 5, 2025

[Merged by Bors] - refactor: don't use lambdas in CoeFun instances #21405

Closed

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 5, 2025

eric-wieser added 2 commits February 5, 2025 04:31

whitespace

aae3cb1

fix

7049fab

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 Feb 5, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 5, 2025

Merge branch 'master' into eric-wieser/toContinuousAddMonoidHom2

3092a7c

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 5, 2025

eric-wieser requested a review from jcommelin February 10, 2025 18:26

jcommelin reviewed Feb 11, 2025

View reviewed changes

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

mathlib-bors bot pushed a commit that referenced this pull request Feb 11, 2025

feat: lemmas about forgetting linearity of ContinuousLinearMap (#21444)

f64125d

Co-authored-by: Eric Wieser <efw@google.com>

mathlib-bors bot changed the title ~~feat: lemmas about forgetting linearity of ContinuousLinearMap~~ [Merged by Bors] - feat: lemmas about forgetting linearity of ContinuousLinearMap Feb 11, 2025

mathlib-bors bot closed this Feb 11, 2025

mathlib-bors bot deleted the eric-wieser/toContinuousAddMonoidHom2 branch February 11, 2025 17:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: lemmas about forgetting linearity of ContinuousLinearMap#21444

[Merged by Bors] - feat: lemmas about forgetting linearity of ContinuousLinearMap#21444
eric-wieser wants to merge 7 commits intomasterfrom
eric-wieser/toContinuousAddMonoidHom2

eric-wieser commented Feb 5, 2025 •

edited by alreadydone

Loading

Uh oh!

github-actions bot commented Feb 5, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 5, 2025

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

eric-wieser commented Feb 5, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 3092a7c8f5

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Feb 5, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

eric-wieser commented Feb 5, 2025 •

edited by alreadydone

Loading

github-actions bot commented Feb 5, 2025 •

edited

Loading