[Merged by Bors] - chore: move results about DivisionMonoid + HasDistribNeg#20551
Closed
YaelDillies wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - chore: move results about DivisionMonoid + HasDistribNeg#20551YaelDillies wants to merge 2 commits intomasterfrom
DivisionMonoid + HasDistribNeg#20551YaelDillies wants to merge 2 commits intomasterfrom
Conversation
This way, we don't have to import fields to use those lemmas
PR summary 76aa5cdcf1
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Module.Basic | 452 | 451 | -1 (-0.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
151 filesMathlib.Topology.Algebra.Monoid Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.Topology.Order.LawsonTopology Mathlib.CategoryTheory.Sites.Pullback Mathlib.Topology.CompactOpen Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Action.Continuous Mathlib.Topology.Compactification.OnePoint Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.Sheaves.Sheaf Mathlib.RingTheory.HahnSeries.Addition Mathlib.Combinatorics.Hall.Basic Mathlib.Topology.Sets.Closeds Mathlib.Data.Int.AbsoluteValue Mathlib.Topology.Order.ScottTopology Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.CategoryTheory.Sites.EpiMono Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.LocalAtTarget Mathlib.Algebra.Module.Basic Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Spectral.Hom Mathlib.Topology.PartialHomeomorph Mathlib.Topology.ClopenBox Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Sheaves.LocalPredicate Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.Topology.Sequences Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Maps.Proper.Basic Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Topology.Sober Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Algebra.Star Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.Homeomorph Mathlib.Topology.ContinuousMap.Basic Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Topology.List Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.Gluing Mathlib.Topology.Sets.Order Mathlib.Topology.Hom.Open Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Topology.FiberPartition Mathlib.Topology.ContinuousMap.Sigma Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.NoetherianSpace Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.Topology.Category.TopCat.Opens Mathlib.CategoryTheory.CofilteredSystem Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.CategoryTheory.Sites.Spaces Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.Topology.Sheaves.Limits Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.JacobsonSpace Mathlib.Topology.Specialization Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Dynamics.Minimal Mathlib.Geometry.RingedSpace.Stalks Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.Topology.Sets.Compacts Mathlib.Topology.UniformSpace.HeineCantor Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.Topology.ApproximateUnit Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.Sheaves.Functors Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.Topology.DiscreteQuotient Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.Sets.Opens Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.Topology.Category.CompHausLike.Limits Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.CategoryTheory.Extensive Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Sheaves.Presheaf Mathlib.CategoryTheory.Adhesive Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.IsLocalHomeomorph Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Category.UniformSpace Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Algebra.Support Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.UniformSpace.Equiv Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.Topology.Sheaves.Stalks Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.QuasiSeparated |
-1 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
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).
10 tasks
Ruben-VandeVelde
approved these changes
Jan 7, 2025
Contributor
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Sure
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
Jan 7, 2025
This way, we don't have to import fields to use those lemmas
Contributor
|
Pull request successfully merged into master. Build succeeded: |
DivisionMonoid + HasDistribNegDivisionMonoid + HasDistribNeg
Julian
added a commit
that referenced
this pull request
Jan 8, 2025
* origin/master: (642 commits) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) feat(Analysis/Analytic): lemmas about `smul` for power series (#19816) chore: don't import algebra in `Data.Multiset.Basic` (#19775) ...
Julian
added a commit
that referenced
this pull request
Jan 8, 2025
* origin/master: (80 commits) chore(CategoryTheory): remove data produced by tactic block (#20565) feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) ...
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
3 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.
This way, we don't have to import fields to use those lemmas