[Merged by Bors] - feat: add {Alg,Linear}Equiv.{prodUnique,uniqueProd}#24168
Closed
[Merged by Bors] - feat: add {Alg,Linear}Equiv.{prodUnique,uniqueProd}#24168
Conversation
PR summary 343aa07748
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Algebra.Prod | 703 | 705 | +2 (+0.28%) |
| Mathlib.LinearAlgebra.Prod | 799 | 801 | +2 (+0.25%) |
Import changes for all files
| Files | Import difference |
|---|---|
85 filesMathlib.Algebra.Algebra.Prod Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.DualNumber Mathlib.Algebra.Exact Mathlib.Algebra.FiveLemma Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Polynomial.ofFn Mathlib.Algebra.Star.Module Mathlib.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.UniformSpace.Dini |
2 |
Declarations diff
++ prodUnique
++ uniqueProd
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).
2 tasks
Member
|
PR title & commit message disagree with the diff. Please update. |
Contributor
Author
|
Indeed, that is why this PR was still labelled WIP. I have added the missing content now - so title, description and diff should now match. |
Contributor
Author
|
@eric-wieser You reviewed the original PR #9105: would you like to take a look at this PR also? The diff should be basically identical. |
Ruben-VandeVelde
approved these changes
May 2, 2025
Contributor
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 6, 2025
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
Contributor
|
Pull request successfully merged into master. Build succeeded: |
riccardobrasca
pushed a commit
that referenced
this pull request
May 7, 2025
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
tannerduve
pushed a commit
that referenced
this pull request
May 13, 2025
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras. Rebased version of #9105. Co-authored-by: @LukasMias
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
4 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.
Adds definitions of linear equivalences for modules M with their left-/right-product with a trivial module M \times 0 and 0 \times M, and analogous statements for Algebras.
Rebased version of #9105.
Co-authored-by: @LukasMias