[Merged by Bors] - feat: add DFinsupp version of Finsupp constructions#25166
Closed
eric-wieser wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - feat: add DFinsupp version of Finsupp constructions#25166eric-wieser wants to merge 2 commits intomasterfrom
DFinsupp version of Finsupp constructions#25166eric-wieser wants to merge 2 commits intomasterfrom
Conversation
PR summary e8672969d5
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.DFinsupp | 973 | 976 | +3 (+0.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.LinearAlgebra.Multilinear.DFinsupp |
1 |
247 filesMathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.DualQuaternion Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.SpanRank Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Expand Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.QuaternionBasis Mathlib.Algebra.Quaternion Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Asymptotics.ExpGrowth Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.IntegerCompl Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Strong Mathlib.Analysis.InnerProductSpace.Affine Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Convex Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.LocallyConvex.AbsConvexOpen Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Unbundled.AlgebraNorm Mathlib.Analysis.Normed.Unbundled.FiniteExtension Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful Mathlib.Analysis.Normed.Unbundled.RingSeminorm Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded Mathlib.Analysis.Normed.Unbundled.SeminormFromConst Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.PSeries Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.CircleMap Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Combinatorics.Additive.Corner.Roth 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.GrowsPolynomially Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Complex.Module Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.Real.Irrational Mathlib.Data.ZMod.QuotientRing Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Dynamics.Newton Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Dynamics.TopologicalEntropy.Subset Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Tower Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.GroupTheory.FreeGroup.GeneratorEquiv Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Dimension.Free Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeAlgebra Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.FreeModule.ModN Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.Defs Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Doubling Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.MulChar.Lemmas Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Pell Mathlib.NumberTheory.Rayleigh Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.VonMangoldt Mathlib.RingTheory.AdicCompletion.Noetherian Mathlib.RingTheory.Adjoin.FG Mathlib.RingTheory.Adjoin.Tower Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.Filtration Mathlib.RingTheory.FinitePresentation Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Quotient Mathlib.RingTheory.Finiteness.Small Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.Henselian Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.RingTheory.Jacobson.Polynomial Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Basic Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.Orzech Mathlib.RingTheory.OrzechProperty Mathlib.RingTheory.Polynomial.Basic Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.PowerSeries.WeierstrassPreparation Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.ReesAlgebra Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.ZMod Mathlib.Tactic.NormNum.Irrational Mathlib.Tactic.ReduceModChar Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Instances.AddCircle.DenseSubgroup Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.RatLemmas Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski |
3 |
Declarations diff
+ domLCongr
+ linearEquivFunOnFintype
+ sigmaCurryLEquiv
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
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).
This was referenced May 25, 2025
Vierkantor
approved these changes
May 29, 2025
Contributor
Vierkantor
left a comment
There was a problem hiding this comment.
Looks good to me, thanks!
bors r+
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 29, 2025
For ease of discovery, I copy the `Finsupp` names rather than the `DirectSum` names.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
DFinsupp version of Finsupp constructionsDFinsupp version of Finsupp constructions
bwehlin
pushed a commit
to bwehlin/mathlib4
that referenced
this pull request
May 31, 2025
…ommunity#25166) For ease of discovery, I copy the `Finsupp` names rather than the `DirectSum` names.
joelriou
pushed a commit
that referenced
this pull request
Jun 8, 2025
For ease of discovery, I copy the `Finsupp` names rather than the `DirectSum` names.
TOMILO87
pushed a commit
that referenced
this pull request
Jun 8, 2025
For ease of discovery, I copy the `Finsupp` names rather than the `DirectSum` names.
callesonne
pushed a commit
to callesonne/mathlib4
that referenced
this pull request
Jul 24, 2025
…ommunity#25166) For ease of discovery, I copy the `Finsupp` names rather than the `DirectSum` names.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
For ease of discovery, I copy the
Finsuppnames rather than theDirectSumnames.