[Merged by Bors] - chore: to_additive various results on groups, group actions #20498

AntoineChambert-Loir · 2025-01-05T21:33:43Z

github-actions · 2025-01-05T21:34:33Z

PR summary dde6eb3927

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ SubAddAction
+ _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate
+ _root_.AddAction.IsBlock.translate

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
1514	1	erw

Current commit dde6eb3927
Reference commit a57f31753d

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies

Thanks for splitting!

Sorry, I got bored halfway through, but there are more to fix. There are also several missing docstrings on the additivised versions

Mathlib/GroupTheory/GroupAction/Pointwise.lean

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Mathlib/GroupTheory/GroupAction/Basic.lean

Mathlib/GroupTheory/GroupAction/Blocks.lean

YaelDillies

Thanks!

maintainer delegate

YaelDillies · 2025-01-06T18:29:04Z

Mathlib/GroupTheory/GroupAction/Blocks.lean

 theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} :
    IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B := by
  refine forall₂_congr fun g₁ g₂ ↦ ?_
  rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
    Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]

+theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate


Suggested change

theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate

theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate

YaelDillies · 2025-01-06T18:30:46Z

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

+/-- A SubAddAction is a set which is closed under scalar multiplication. -/
+structure SubAddAction (R : Type u) (M : Type v) [VAdd R M] : Type v where
+  /-- The underlying set of a `SubAddAction`. -/
+  carrier : Set M
+  /-- The carrier set is closed under scalar multiplication. -/
+  vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier
+
+attribute [to_additive] SubMulAction


Can you swap SubAddAction and SubMulAction around and tag SubMulAction with to_additive straight away?

github-actions · 2025-01-06T18:31:37Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

fpvandoorn · 2025-01-06T19:55:27Z

bors d+

mathlib-bors · 2025-01-06T19:55:29Z

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

AntoineChambert-Loir · 2025-01-06T22:53:21Z

bors r+ Le 6 janvier 2025 20:55:52 GMT+01:00, "mathlib-bors[bot]" ***@***.***> a écrit :

…

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with `bors r+`. More detailed instructions are available [here](https://bors.tech/documentation/getting-started/#reviewing-pull-requests). -- Reply to this email directly or view it on GitHub: #20498 (comment) You are receiving this because you authored the thread. Message ID: ***@***.***>

mathlib-bors · 2025-01-06T23:47:08Z

Pull request successfully merged into master.

Build succeeded:

YaelDillies · 2025-01-07T07:59:00Z

@AntoineChambert-Loir, you didn't address my final comments (probably because you didn't see them via the email system)

AntoineChambert-Loir · 2025-01-07T11:43:58Z

i' sorry, can you please send it back to me so that i can address it immediately Le 7 janvier 2025 08:59:22 GMT+01:00, "Yaël Dillies" ***@***.***> a écrit :

…

@AntoineChambert-Loir, you didn't address my final comments (probably because you didn't see them via the email system) -- Reply to this email directly or view it on GitHub: #20498 (comment) You are receiving this because you were mentioned. Message ID: ***@***.***>

@YaelDillies

Two adjustments to #20498 that had been requested by @YaelDillies but hadn't been implemented on time before merge.

Two adjustments to #20498 that had been requested by Yaël but hadn't been implemented on time before merge.

AntoineChambert-Loir added 4 commits January 5, 2025 22:24

to-additive on Blocks

92a65e4

to additive GroupAction

1acc2cc

to additive Pointwise

e51ecb7

to additive SubMulAction

858d1e4

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 5, 2025

AntoineChambert-Loir mentioned this pull request Jan 5, 2025

feat(GroupTheory/GroupAction/Primitive) #12052

Open

7 tasks

YaelDillies changed the title ~~Feat: to_additive various results on groups, group actions~~ chore: to_additive various results on groups, group actions Jan 5, 2025

YaelDillies reviewed Jan 5, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 5, 2025

adjust attr=simp and remove one lemma

d996233

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

AntoineChambert-Loir added 2 commits January 6, 2025 10:42

add one forgotten to_additive

47135a9

adjust one deprecated lemma

e02914a

YaelDillies reviewed Jan 6, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

add doc, better formatting

dde6eb3

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

YaelDillies approved these changes Jan 6, 2025

View reviewed changes

github-actions bot added the maintainer-merge label Jan 6, 2025

leanprover-community-mathlib4-bot added the delegated label Jan 6, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025

chore: to_additive various results on groups, group actions (#20498)

d4a7b67

mathlib-bors bot changed the title ~~chore: to_additive various results on groups, group actions~~ [Merged by Bors] - chore: to_additive various results on groups, group actions Jan 6, 2025

mathlib-bors bot closed this Jan 6, 2025

mathlib-bors bot deleted the ACL/Primitive-1 branch January 6, 2025 23:47

AntoineChambert-Loir mentioned this pull request Jan 7, 2025

[Merged by Bors] - chore: to_additive various results on groups, group actions #20547

Closed

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025

chore: to_additive various results on groups, group actions (#20547)

9abadcd

Two adjustments to #20498 that had been requested by @YaelDillies but hadn't been implemented on time before merge.

mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025

chore: to_additive various results on groups, group actions (#20547)

db72aff

Two adjustments to #20498 that had been requested by Yaël but hadn't been implemented on time before merge.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: to_additive various results on groups, group actions #20498

[Merged by Bors] - chore: to_additive various results on groups, group actions #20498

AntoineChambert-Loir commented Jan 5, 2025

github-actions bot commented Jan 5, 2025 •

edited

Loading

Declarations diff

YaelDillies left a comment •

edited

Loading

YaelDillies left a comment

YaelDillies Jan 6, 2025

YaelDillies Jan 6, 2025

github-actions bot commented Jan 6, 2025

fpvandoorn commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

AntoineChambert-Loir commented Jan 6, 2025 via email

mathlib-bors bot commented Jan 6, 2025

YaelDillies commented Jan 7, 2025

AntoineChambert-Loir commented Jan 7, 2025 via email

	theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate
	theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate

[Merged by Bors] - chore: to_additive various results on groups, group actions #20498

[Merged by Bors] - chore: to_additive various results on groups, group actions #20498

Conversation

AntoineChambert-Loir commented Jan 5, 2025

github-actions bot commented Jan 5, 2025 • edited Loading

PR summary dde6eb3927

Import changes for modified files

Declarations diff

YaelDillies left a comment • edited Loading

Choose a reason for hiding this comment

YaelDillies left a comment

Choose a reason for hiding this comment

YaelDillies Jan 6, 2025

Choose a reason for hiding this comment

YaelDillies Jan 6, 2025

Choose a reason for hiding this comment

github-actions bot commented Jan 6, 2025

fpvandoorn commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

AntoineChambert-Loir commented Jan 6, 2025 via email

mathlib-bors bot commented Jan 6, 2025

YaelDillies commented Jan 7, 2025

AntoineChambert-Loir commented Jan 7, 2025 via email

github-actions bot commented Jan 5, 2025 •

edited

Loading

YaelDillies left a comment •

edited

Loading