[Merged by Bors] - chore: split Algebra/BigOperators/Group/{Multiset,Finset}#20629
[Merged by Bors] - chore: split Algebra/BigOperators/Group/{Multiset,Finset}#20629
Algebra/BigOperators/Group/{Multiset,Finset}#20629Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
Still needs a |
PR summary 6dc03030e4
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Nat.GCD.BigOperators | 512 | 451 | -61 (-11.91%) |
| Mathlib.Algebra.Regular.Pow | 521 | 460 | -61 (-11.71%) |
| Mathlib.Algebra.BigOperators.RingEquiv | 523 | 462 | -61 (-11.66%) |
| Mathlib.Algebra.Star.BigOperators | 578 | 518 | -60 (-10.38%) |
| Mathlib.GroupTheory.Congruence.BigOperators | 513 | 467 | -46 (-8.97%) |
| Mathlib.Deprecated.Submonoid | 524 | 480 | -44 (-8.40%) |
| Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset | 425 | 390 | -35 (-8.24%) |
| Mathlib.Algebra.Module.Submodule.LinearMap | 590 | 548 | -42 (-7.12%) |
| Mathlib.CategoryTheory.Preadditive.Basic | 645 | 600 | -45 (-6.98%) |
| Mathlib.Data.Rat.BigOperators | 598 | 561 | -37 (-6.19%) |
| Mathlib.Logic.Godel.GodelBetaFunction | 555 | 525 | -30 (-5.41%) |
| Mathlib.CategoryTheory.Subobject.Lattice | 663 | 632 | -31 (-4.68%) |
| Mathlib.RingTheory.Localization.Defs | 688 | 659 | -29 (-4.22%) |
| Mathlib.Algebra.Order.BigOperators.Ring.Multiset | 463 | 444 | -19 (-4.10%) |
| Mathlib.GroupTheory.QuotientGroup.Basic | 658 | 655 | -3 (-0.46%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 3873 files with changed transitive imports taking up over 168453 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 3102 | 1 | total LoC in Deprecated files |
Current commit 6dc03030e4
Reference commit 039d0c7642
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).
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
I tried to fix the matrix test again; otherwise this seems sensible enough to me.
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
Nice decrease! Can we get a few sentences explanation of the split in the PR description? |
| refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop | ||
|
|
||
| @[to_additive] | ||
| lemma prod_ite_of_false {p : α → Prop} {_ : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f g : α → β) : |
There was a problem hiding this comment.
May I suggest that something is wrong if the ite and dite versions of the same lemma find themselves in different files?
There was a problem hiding this comment.
I disagree that this is wrong, but have postponed the dite versions into the file with the ite versions.
Very happy if someone wants to go through and reduce the import requirements of proofs and then move lemmas upstream, but that's not on the agenda here.
There was a problem hiding this comment.
What "agenda"? What's the greater context for reducing imports here?
There was a problem hiding this comment.
"not on the agenda" meaning I'm not interesting in rewriting proofs in this file during this PR.
There was a problem hiding this comment.
I'm just trying to understand why you are doing this split 😅
|
Thanks 🎉 bors merge |
Follow on from #20625. Keeps only what is possible with the minimal imports required for the definitions themselves in the `Defs` file, and everything else moves to `Lemmas`. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
Algebra/BigOperators/Group/{Multiset,Finset}Algebra/BigOperators/Group/{Multiset,Finset}
Follow on from #20625.
Keeps only what is possible with the minimal imports required for the definitions themselves in the
Defsfile, and everything else moves toLemmas.