[Merged by Bors] - chore(LinearIndependent): generalize to semirings #20480
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
PR summary 374f5eda76
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.LinearIndependent | 880 | 882 | +2 (+0.23%) |
| Mathlib.LinearAlgebra.Dimension.Basic | 899 | 901 | +2 (+0.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
1579 filesMathlib.Algebra.Homology.ShortComplex.Ab Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.Analysis.MeanInequalitiesPow Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Topology.Algebra.Module.Simple Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.Localization.AtPrime Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.RingTheory.AlgebraTower Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Analysis.Convex.AmpleSet Mathlib.Probability.Variance Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.RingTheory.Noetherian.Orzech Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Analysis.Analytic.OfScalars Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Algebra.Category.Grp.AB Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Analysis.Calculus.Deriv.Add Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.FieldTheory.Laurent Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.NumberTheory.GaussSum Mathlib.Algebra.Colimit.TensorProduct Mathlib.Analysis.Convex.Birkhoff Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Condensed.Limits Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.CategoryTheory.Abelian.Ext Mathlib.Algebra.Category.ModuleCat.AB Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Analysis.Complex.AbsMax Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.WittVector.InitTail Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.Analysis.Convex.Topology Mathlib.Geometry.Manifold.Complex Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Algebra.DirectSum.Module Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.RingTheory.Derivation.Lie Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Analysis.Complex.HalfPlane Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.Isometry Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.MeasureTheory.Function.L2Space Mathlib.Topology.VectorBundle.Hom Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Analysis.SpecialFunctions.Exp Mathlib.RingTheory.Polynomial.Quotient Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.PID Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Algebra.MvPolynomial.Funext Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.ModelTheory.Algebra.Ring.Definability Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.FieldTheory.Isaacs Mathlib.LinearAlgebra.DFinsupp Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Topology.Compactification.OnePointEquiv Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.NumberTheory.LSeries.ZMod Mathlib.RingTheory.Bialgebra.Hom Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Artinian.Ring Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Topology.Sheaves.CommRingCat Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.RingTheory.Localization.BaseChange Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.FieldTheory.Normal Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.RingTheory.KrullDimension.Field Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Probability.Martingale.Upcrossing Mathlib.RingTheory.Coalgebra.Basic Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Condensed.AB Mathlib.Algebra.Quaternion Mathlib.Condensed.Explicit Mathlib.Data.Nat.Choose.Lucas Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Norm.Defs Mathlib.RingTheory.Kaehler.Polynomial Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Analysis.RCLike.Inner Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.WittVector.Identities Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Condensed.Discrete.Characterization Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.RingTheory.Localization.Integral Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Lie.Derivation.Killing Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.Complex.Circle Mathlib.RingTheory.Artinian.Module Mathlib.Data.ZMod.Quotient Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Analysis.InnerProductSpace.Dual Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.GroupTheory.Nilpotent Mathlib.RingTheory.Bialgebra.Basic Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Algebra.Lie.Free Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Convex.Intrinsic Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.RingTheory.Invariant Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.AlgebraicGeometry.Sites.Small Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.RingTheory.RingHom.Finite Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.EssentialFiniteness Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.LinearAlgebra.PerfectPairing Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.LSeries.Deriv Mathlib.AlgebraicGeometry.ResidueField Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.RingTheory.Ideal.Cotangent Mathlib.Analysis.Fourier.AddCircle Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.RingTheory.Flat.Localization Mathlib.Topology.ContinuousMap.Compact Mathlib.RingTheory.Nullstellensatz Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.RingTheory.Polynomial.Radical Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Algebra.Lie.IdealOperations Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.Category.ModuleCat.Products Mathlib.AlgebraicGeometry.Over Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Algebra.Module.Presentation.Free Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Analysis.Calculus.Taylor Mathlib.MeasureTheory.Group.AddCircle Mathlib.RingTheory.DualNumber Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.RingTheory.Noetherian.Basic Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Algebra.Colimit.Finiteness Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.RingTheory.Algebraic.Basic Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.RingTheory.Presentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Algebra.Lie.DirectSum Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Probability.Martingale.Basic Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.RingTheory.Coprime.Ideal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.Normed.Module.Span Mathlib.Algebra.Polynomial.Expand Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.LinearAlgebra.FiniteDimensional Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.FieldTheory.Extension Mathlib.LinearAlgebra.Orientation Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.LinearAlgebra.FreeModule.Int Mathlib.Algebra.DirectSum.Internal Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.Topology.UrysohnsBounded Mathlib.Combinatorics.Configuration Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.AlgebraicGeometry.Properties Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Data.Real.Pi.Irrational Mathlib.RingTheory.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Algebra.DirectSum.Idempotents Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Coalgebra.Hom Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Condensed.Solid Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.RingTheory.Unramified.Pi Mathlib.Algebra.Lie.LieTheorem Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.Condensed.Discrete.Module Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Generators Mathlib.RingTheory.Adjoin.Tower Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Data.Complex.Determinant Mathlib.Analysis.Complex.OperatorNorm Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.FieldTheory.Relrank Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Algebra.DirectSum.Decomposition Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Polynomial.Bernstein Mathlib.AlgebraicGeometry.Cover.Over Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Algebra.LinearRecurrence Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.NumberTheory.MulChar.Duality Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.Complex.ReImTopology Mathlib.RingTheory.ZMod Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Algebra.Module.Projective Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.CategoryTheory.Abelian.Injective Mathlib.Dynamics.Newton Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RepresentationTheory.Basic Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.GroupTheory.CosetCover Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.CategoryTheory.Abelian.Projective Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Algebra.Polynomial.Derivation Mathlib.RingTheory.Algebraic.Integral Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Probability.Distributions.Uniform Mathlib.RingTheory.MvPolynomial Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.GroupTheory.Torsion Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Algebra.DirectSum.Finsupp Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.Analysis.Convex.Between Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Algebra.AlgebraicCard Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.Analysis.MeanInequalities Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.RingTheory.RingHom.Integral Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.AlgebraicGeometry.AffineSpace Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Combinatorics.Additive.Randomisation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Algebra.Polynomial.Module.Basic Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.RingTheory.SurjectiveOnStalks Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.Convex.Independent Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.LinearAlgebra.Matrix.BaseChange Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.RingTheory.LocalProperties.Exactness Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.RingTheory.OrzechProperty Mathlib.Analysis.BoxIntegral.Basic Mathlib.RingTheory.Valuation.LocalSubring Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.RingTheory.Polynomial.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Algebra.Lie.Abelian Mathlib.LinearAlgebra.SesquilinearForm Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.RingTheory.HopfAlgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.RingTheory.Discriminant Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.RingTheory.ReesAlgebra Mathlib.Analysis.Analytic.Meromorphic Mathlib.Algebra.Module.PID Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Analysis.Convex.KreinMilman Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.RingTheory.Polynomial.Wronskian Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.NormedSpace.Extr Mathlib.NumberTheory.ClassNumber.Finite Mathlib.FieldTheory.Finiteness Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Analysis.InnerProductSpace.Defs Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.Analysis.Convex.Normed Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Extension Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.NumberTheory.LSeries.Positivity Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.RingTheory.Localization.Free Mathlib.Analysis.Analytic.Linear Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Algebra.Module.Torsion Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.Complex Mathlib.Algebra.Jordan.Basic Mathlib.AlgebraicGeometry.AffineScheme Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.NumberTheory.Padics.RingHoms Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.KrullDimension.Basic Mathlib.Algebra.Category.Grp.Images Mathlib.FieldTheory.Separable Mathlib.Condensed.Light.AB Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.Algebra.Module.FinitePresentation Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Topology.Algebra.PontryaginDual Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.Topology.MetricSpace.Holder Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.RingTheory.WittVector.Frobenius Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Algebra.Colimit.Module Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.Analysis.NormedSpace.DualNumber Mathlib.NumberTheory.Pell Mathlib.FieldTheory.AlgebraicClosure Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Condensed.Light.Limits Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.RingTheory.Jacobson.Ring Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Tactic.ReduceModChar Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Topology.VectorBundle.Constructions Mathlib.GroupTheory.Transfer Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.AlgebraicGeometry.PrimeSpectrum.Polynomial Mathlib.RingTheory.Smooth.Kaehler Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.RingTheory.RingHom.Locally Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RepresentationTheory.FDRep Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Analysis.Analytic.Composition Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.RingTheory.Trace.Quotient Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.Calculus.Implicit Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.FieldTheory.NormalClosure Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.LinearAlgebra.Reflection Mathlib.RingTheory.Adjoin.Dimension Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.Analysis.Convex.TotallyBounded Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.RingTheory.LocalProperties.Reduced Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Algebra.Lie.Derivation.Basic Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Algebra.Category.CoalgebraCat.Monoidal Mathlib.Probability.Independence.Integrable Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.RingTheory.Coalgebra.Equiv Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Homology.LocalCohomology Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.Data.Complex.Module Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.FieldTheory.KummerExtension Mathlib.NumberTheory.LucasPrimality Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.Analysis.Convex.Jensen Mathlib.RingTheory.Jacobson.Polynomial Mathlib.Topology.Instances.Irrational Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Topology.Algebra.Module.Determinant Mathlib.SetTheory.Cardinal.Free Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.NumberTheory.BernoulliPolynomials Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.RingHomProperties Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.Category.Ring.Constructions Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.LinearAlgebra.Dimension.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Lie.BaseChange Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.LinearAlgebra.Dual Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Convex.Combination Mathlib.LinearAlgebra.Matrix.Basis Mathlib.RingTheory.Bialgebra.Equiv Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.NumberTheory.PrimesCongruentOne Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.LinearAlgebra.Basis.Basic Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.RingTheory.Localization.Module Mathlib.Probability.Process.Adapted Mathlib.Algebra.Lie.Subalgebra Mathlib.Analysis.Convex.Cone.Proper Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Analytic.Within Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Visible Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.MeasureTheory.Integral.Pi Mathlib.RingTheory.LocalProperties.Basic Mathlib.NumberTheory.NumberField.House Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Algebra.Lie.Solvable Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Condensed.Epi Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Probability.Process.Filtration Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.LinearAlgebra.TensorPower Mathlib.RingTheory.Valuation.Minpoly Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.RingTheory.Artinian.Instances Mathlib.NumberTheory.Bernoulli Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.LinearAlgebra.Determinant Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.NormedSpace.Real Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.RingTheory.FiniteLength Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Algebra.Lie.Rank Mathlib.Probability.Kernel.Condexp Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.GroupTheory.Order.Min Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.Algebra.Lie.Classical Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Polynomial.Bivariate Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.RingTheory.MaximalSpectrum Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.FiniteType Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Analysis.NormedSpace.BallAction Mathlib.NumberTheory.Padics.ProperSpace Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.RingTheory.Finiteness.Projective Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.NormedSpace.Connected Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.RingTheory.IntegralDomain Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Algebra.DirectSum.Algebra Mathlib.Analysis.ODE.PicardLindelof Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.FieldTheory.Tower Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.RingTheory.TensorProduct.Free Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Analytic.Polynomial Mathlib.RingTheory.PrimeSpectrum Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Algebra.CharP.MixedCharZero Mathlib.GroupTheory.Frattini Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Algebra.MvPolynomial.Invertible Mathlib.GroupTheory.PGroup Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.RingTheory.RingHom.Surjective Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.Dimension.Finite Mathlib.RingTheory.DedekindDomain.PID Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.Convex.StoneSeparation Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Lie.TensorProduct Mathlib.RingTheory.Norm.Transitivity Mathlib.FieldTheory.SplittingField.Construction Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.RingTheory.Support Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Unramified.Finite Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.RepresentationTheory.Maschke Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.GroupTheory.Schreier Mathlib.RingTheory.NormTrace Mathlib.MeasureTheory.Measure.Complex Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Geometry.Manifold.Metrizable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Lie.InvariantForm Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.FieldTheory.RatFunc.Degree Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Algebra.Polynomial.Module.AEval Mathlib.NumberTheory.FLT.MasonStothers Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.RingTheory.Perfection Mathlib.Algebra.Homology.ConcreteCategory Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.Probability.CDF Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.LinearAlgebra.StdBasis Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.LinearAlgebra.Matrix.Dual Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Analysis.Normed.Module.Completion Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.RingTheory.LocalProperties.Projective Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Probability.Martingale.Centering Mathlib.Algebra.Lie.OfAssociative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.LinearAlgebra.Matrix.Block Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Data.Nat.Factorial.SuperFactorial |
1 |
49 filesMathlib.Topology.Homotopy.Contractible Mathlib.Data.Matrix.DoublyStochastic Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.Analysis.Seminorm Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Convex.Slope Mathlib.Topology.Homotopy.Path Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.Analysis.LocallyConvex.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Topology.Homotopy.Product Mathlib.Analysis.Asymptotics.TVS Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.Analysis.Convex.Cone.Extension Mathlib.LinearAlgebra.CrossProduct Mathlib.Analysis.Convex.Join Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.LinearIndependent Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Analysis.Convex.EGauge Mathlib.LinearAlgebra.Ray Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.Contractible Mathlib.LinearAlgebra.Alternating.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Convex.Function Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.Analysis.Convex.Exposed Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular |
2 |
Declarations diff
+ Fintype.linearIndependent_iff'ₛ
+ Fintype.linearIndependent_iff_injective
+ Fintype.linearIndependent_iffₛ
+ Fintype.not_linearIndependent_iffₛ
+ LinearIndependent.image_subtypeₛ
+ LinearIndependent.map_injOn
+ LinearIndependent.map_of_injective_injectiveₛ
+ LinearIndependent.not_smul_mem_span
+ LinearIndependent.pair_iffₛ
+ LinearMap.linearIndependent_iff_of_disjoint
+ LinearMap.linearIndependent_iff_of_injOn
+ _root_.Set.InjOn.injective_iff
+ linearCombination_restrict
+ linearDependent_comp_subtype'ₛ
+ linearDependent_comp_subtypeₛ
+ linearIndependent_comp_subtypeₛ
+ linearIndependent_iff''ₛ
+ linearIndependent_iff'ₛ
+ linearIndependent_iff_linearCombinationOnₛ
+ linearIndependent_iffₛ
+ linearIndependent_restrict_iff
+ linearIndependent_subtypeₛ
+ not_linearIndependent_iffₛ
+ subtypeDomain_eq_iff
+ subtypeDomain_eq_iff_forall
+ supportedEquivFinsupp_symm_apply_coe
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.02)
| Current number | Change | Type |
|---|---|---|
| 59 | 1 | large files |
Current commit 374f5eda76
Reference commit a36b4f2f1d
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).
eric-wieser
reviewed
Jan 5, 2025
| simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp, hf_inj.of_comp_iff] | ||
|
|
||
| /-- An injective linear map sends linearly independent families of vectors to linearly independent | ||
| families of vectors. See also `LinearIndependent.map` for a more general statement. -/ |
There was a problem hiding this comment.
The generality is now incomparable! My draft at #18503 restates map as
theorem LinearIndependent.map (hv : LinearIndependent R v) {f : M →ₗ[R] M'}
(hf : Set.InjOn f (span R (range v))):
LinearIndependent R (f ∘ v) := bywhich keeps the support for semirings
There was a problem hiding this comment.
This is nice, I'd certainly adopt it.
There was a problem hiding this comment.
Perhaps to make things reviewable, we should:
- Pre-emptively restate the theorems such that they could be generalized to semirings (a spin off PR)
- Move all the theorems around without changing their statement (this PR)
Otherwise I think we might want to spin up leaff here...
There was a problem hiding this comment.
Is it that hard to review? Declaration diff shows no decls are removed. New decls with a s subscript are straightforward generalization of the ring version without the s.
There was a problem hiding this comment.
I think I've incorporated all generalizations from your PR, and I added you as a co-author.
There was a problem hiding this comment.
If you're worried about the accuracy of docstrings:
(1) No decls are removed; for the existing decls that are moved, the docstrings are moved together. Since the statements don't change I think the docstrings probably also need not change.
(2) Most new decls in the file LinearIndependent are modified version of existing decls, and carry the docstrings (whenever they exist) from the existing decls. I have now checked all docstrings of new decls and modified them to match the (Semiring-specific) new statements.
There was a problem hiding this comment.
Is it that hard to review? Declaration diff shows no decls are removed. New decls with a s subscript are straightforward generalization of the ring version without the s.
I agree with @eric-wieser that it would be nice to have leaff working on this. But afaik leaff isn't really ready for that yet, right?
Given that no decls were removed, I suggest we just move forward with this.
bors merge
alreadydone
force-pushed
the
Semiring_LinearIndependent
branch
from
6125551 to
374f5ed
Compare
1 task
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 6, 2025
After the definition is changed in #18426, many results can now be generalized to semirings. Co-authored-by: Eric Wieser <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Julian
added a commit
that referenced
this pull request
Jan 6, 2025
* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...
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.
After the definition is changed in #18426, many results can now be generalized to semirings.
Co-authored-by: Eric Wieser [email protected]