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

Two adjustments to #20498 that had been requested by Yaël but hadn't been implemented on time before merge.
leanprover-community · Jan 7, 2025 · db72aff · db72aff
1 parent 01e6638
commit db72aff
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 11 deletions.
diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean
@@ -311,7 +311,7 @@ theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} :
   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
+theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate
     {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X}
     {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) :
     AddAction.IsBlock (H.map (AddAut.conj g).toAddMonoidHom) (g +ᵥ B) := by
@@ -330,7 +330,7 @@ theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate
   erw [AddAut.conj_apply]
   simp
 
-@[to_additive existing AddAction.IsBlock.of_addsubgroup_of_conjugate]
+@[to_additive existing]
 theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) :
     IsBlock (H.map (MulAut.conj g).toMonoidHom) (g • B) := by
   rw [isBlock_iff_smul_eq_or_disjoint]
@@ -353,7 +353,7 @@ theorem _root_.AddAction.IsBlock.translate
     AddAction.IsBlock G (g +ᵥ B) := by
   rw [← AddAction.isBlock_top] at hB ⊢
   rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
-  · apply AddAction.IsBlock.of_addsubgroup_of_conjugate
+  · apply AddAction.IsBlock.of_addSubgroup_of_conjugate
     rwa [AddSubgroup.comap_top]
   · exact (AddAut.conj g).surjective
 

diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@@ -154,21 +154,20 @@ end OfTower
 
 end SetLike
 
-/-- A SubMulAction is a set which is closed under scalar multiplication. -/
-structure SubMulAction (R : Type u) (M : Type v) [SMul R M] : Type v where
-  /-- The underlying set of a `SubMulAction`. -/
-  carrier : Set M
-  /-- The carrier set is closed under scalar multiplication. -/
-  smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier
-
 /-- 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
+/-- A SubMulAction is a set which is closed under scalar multiplication. -/
+@[to_additive]
+structure SubMulAction (R : Type u) (M : Type v) [SMul R M] : Type v where
+  /-- The underlying set of a `SubMulAction`. -/
+  carrier : Set M
+  /-- The carrier set is closed under scalar multiplication. -/
+  smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier
 
 namespace SubMulAction