[Merged by Bors] - feat: s⁻¹.encard = s.encard#19400
[Merged by Bors] - feat: s⁻¹.encard = s.encard#19400YaelDillies wants to merge 2 commits intomasterfrom
s⁻¹.encard = s.encard#19400Conversation
From Kneser (LeanCamCombi)
PR summary 41d5dffad1
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Group.Pointwise.Set.Card | 750 | 751 | +1 (+0.13%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Group.Pointwise.Set.Card Mathlib.RingTheory.Adjoin.Dimension |
1 |
Declarations diff
+ encard_inv
+ encard_smul_set
+ ncard_inv
+ ncard_smul_set
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).
| @[to_additive (attr := simp)] | ||
| lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by simp [encard, PartENat.card] | ||
|
|
||
| @[to_additive (attr := simp)] | ||
| lemma ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard := by simp [ncard] | ||
|
|
||
| @[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_inv := natCard_inv |
There was a problem hiding this comment.
| @[to_additive (attr := simp)] | |
| lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by simp [encard, PartENat.card] | |
| @[to_additive (attr := simp)] | |
| lemma ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard := by simp [ncard] | |
| @[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_inv := natCard_inv | |
| @[to_additive (attr := deprecated (since := "2024-09-30"))] alias card_inv := natCard_inv | |
| @[to_additive (attr := simp)] | |
| lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by simp [encard, PartENat.card] | |
| @[to_additive (attr := simp)] | |
| lemma ncard_inv (s : Set G) : s⁻¹.ncard = s.ncard := by simp [ncard] |
to keep the alias closer
There was a problem hiding this comment.
I was purposefully flushing the aliases to the bottom because they are mostly just noise. What's your rationale for wanting aliases closer to the declaration they already reference?
There was a problem hiding this comment.
Since they reference the declaration, it's easier to identify which lemma is being referenced rather than needing to scroll to find it. In addition, in the docs, it's useful to have these lemmas next to each other rather than having other things in between.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
s⁻¹.encard = s.encards⁻¹.encard = s.encard
From Kneser (LeanCamCombi)