Documentation

Mathlib.Algebra.Group.Subgroup.Pointwise

Pointwise instances on Subgroup and AddSubgroups #

This file provides the actions

which matches the action of Set.mulActionSet.

These actions are available in the Pointwise locale.

Implementation notes #

The pointwise section of this file is almost identical to the file Mathlib/Algebra/Group/Submonoid/Pointwise.lean. Where possible, try to keep them in sync.

source
@[simp]
theorem inv_coe_set {G : Type u_2} {S : Type u_4} [InvolutiveInv G] [SetLike S G] [InvMemClass S G] {H : S} :
(↑H)⁻¹ = ↑H
source
@[simp]
theorem neg_coe_set {G : Type u_2} {S : Type u_4} [InvolutiveNeg G] [SetLike S G] [NegMemClass S G] {H : S} :
-↑H = ↑H
source
@[simp]
theorem smul_coe_set {G : Type u_2} {S : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
a • ↑s = ↑s
source
@[simp]
theorem vadd_coe_set {G : Type u_2} {S : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
a +ᵥ ↑s = ↑s
source
theorem coe_set_eq_one {G : Type u_2} [Group G] {s : Subgroup G} :
↑s = 1 ↔ s = ⊥
source
theorem coe_set_eq_zero {G : Type u_2} [AddGroup G] {s : AddSubgroup G} :
↑s = 0 ↔ s = ⊥
source
@[simp]
theorem op_smul_coe_set {G : Type u_2} {S : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
MulOpposite.op a • ↑s = ↑s
source
@[simp]
theorem op_vadd_coe_set {G : Type u_2} {S : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
AddOpposite.op a +ᵥ ↑s = ↑s
source
@[simp]
theorem coe_div_coe {G : Type u_2} {S : Type u_4} [SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) :
↑H / ↑H = ↑H
source
@[simp]
theorem coe_sub_coe {G : Type u_2} {S : Type u_4} [SetLike S G] [SubtractionMonoid G] [AddSubgroupClass S G] (H : S) :
↑H - ↑H = ↑H
source
@[simp]
theorem Set.mul_subgroupClosure {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) :
s * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
source
@[simp]
theorem Set.add_addSubgroupClosure {G : Type u_2} [AddGroup G] {s : Set G} (hs : s.Nonempty) :
s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
source
@[simp]
theorem Set.subgroupClosure_mul {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) :
↑(Subgroup.closure s) * s = ↑(Subgroup.closure s)
source
@[simp]
theorem Set.addSubgroupClosure_add {G : Type u_2} [AddGroup G] {s : Set G} (hs : s.Nonempty) :
↑(AddSubgroup.closure s) + s = ↑(AddSubgroup.closure s)
source
@[simp]
theorem Set.pow_mul_subgroupClosure {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) (n : ℕ) :
s ^ n * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
source
@[simp]
theorem Set.nsmul_add_addSubgroupClosure {G : Type u_2} [AddGroup G] {s : Set G} (hs : s.Nonempty) (n : ℕ) :
n • s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
source
@[simp]
theorem Set.subgroupClosure_mul_pow {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) (n : ℕ) :
↑(Subgroup.closure s) * s ^ n = ↑(Subgroup.closure s)
source
@[simp]
theorem Set.addSubgroupClosure_add_nsmul {G : Type u_2} [AddGroup G] {s : Set G} (hs : s.Nonempty) (n : ℕ) :
↑(AddSubgroup.closure s) + n • s = ↑(AddSubgroup.closure s)
source
@[simp]
theorem Subgroup.inv_subset_closure {G : Type u_2} [Group G] (S : Set G) :
S⁻¹ ⊆ ↑(closure S)
source
@[simp]
theorem AddSubgroup.neg_subset_closure {G : Type u_2} [AddGroup G] (S : Set G) :
-S ⊆ ↑(closure S)
source
theorem Subgroup.closure_toSubmonoid {G : Type u_2} [Group G] (S : Set G) :
(closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
source
theorem AddSubgroup.closure_toAddSubmonoid {G : Type u_2} [AddGroup G] (S : Set G) :
(closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)
source
theorem Subgroup.toSubmonoid_zpowers {G : Type u_2} [Group G] (g : G) :
(zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹
source
theorem AddSubgroup.toAddSubmonoid_zmultiples {G : Type u_2} [AddGroup G] (g : G) :
(zmultiples g).toAddSubmonoid = AddSubmonoid.multiples g ⊔ AddSubmonoid.multiples (-g)
source
theorem Submonoid.powers_le_zpowers {G : Type u_2} [Group G] (g : G) :
powers g ≤ (Subgroup.zpowers g).toSubmonoid
source
theorem AddSubmonoid.multiples_le_zmultiples {G : Type u_2} [AddGroup G] (g : G) :
multiples g ≤ (AddSubgroup.zmultiples g).toAddSubmonoid
source
theorem Subgroup.closure_induction_left {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x ∈ closure s → Prop} (one : p 1 ⋯) (mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯) (inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯) {x : G} (h : x ∈ closure s) :
p x h

For subgroups generated by a single element, see the simpler zpow_induction_left.

source
theorem AddSubgroup.closure_induction_left {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x ∈ closure s → Prop} (zero : p 0 ⋯) (add_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x + y) ⋯) (neg_add_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (-x + y) ⋯) {x : G} (h : x ∈ closure s) :
p x h

For additive subgroups generated by a single element, see the simpler zsmul_induction_left.

source
theorem Subgroup.closure_induction_right {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x ∈ closure s → Prop} (one : p 1 ⋯) (mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯) (mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯) {x : G} (h : x ∈ closure s) :
p x h

For subgroups generated by a single element, see the simpler zpow_induction_right.

source
theorem AddSubgroup.closure_induction_right {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x ∈ closure s → Prop} (zero : p 0 ⋯) (add_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯) (add_neg_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯) {x : G} (h : x ∈ closure s) :
p x h

For additive subgroups generated by a single element, see the simpler zsmul_induction_right.

source
@[simp]
theorem Subgroup.closure_inv {G : Type u_2} [Group G] (s : Set G) :
closure s⁻¹ = closure s
source
@[simp]
theorem AddSubgroup.closure_neg {G : Type u_2} [AddGroup G] (s : Set G) :
closure (-s) = closure s
source
@[simp]
theorem Subgroup.closure_singleton_inv {G : Type u_2} [Group G] (x : G) :
closure {x⁻¹} = closure {x}
source
@[simp]
theorem AddSubgroup.closure_singleton_neg {G : Type u_2} [AddGroup G] (x : G) :
closure {-x} = closure {x}
source
theorem Subgroup.closure_induction'' {G : Type u_2} [Group G] {s : Set G} {p : (g : G) → g ∈ closure s → Prop} (mem : ∀ (x : G) (hx : x ∈ s), p x ⋯) (inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯) {x : G} (h : x ∈ closure s) :
p x h

An induction principle for closure membership. If p holds for 1 and all elements of k and their inverse, and is preserved under multiplication, then p holds for all elements of the closure of k.

source
theorem AddSubgroup.closure_induction'' {G : Type u_2} [AddGroup G] {s : Set G} {p : (g : G) → g ∈ closure s → Prop} (mem : ∀ (x : G) (hx : x ∈ s), p x ⋯) (neg_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯) (zero : p 0 ⋯) (add : ∀ (x y : G) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯) {x : G} (h : x ∈ closure s) :
p x h

An induction principle for additive closure membership. If p holds for 0 and all elements of k and their negation, and is preserved under addition, then p holds for all elements of the additive closure of k.

source
theorem Subgroup.iSup_induction {G : Type u_2} [Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x ∈ S i, C x) (one : C 1) (mul : ∀ (x y : G), C x → C y → C (x * y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 1 and all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

source
theorem AddSubgroup.iSup_induction {G : Type u_2} [AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x ∈ S i, C x) (zero : C 0) (add : ∀ (x y : G), C x → C y → C (x + y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds for 0 and all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

source
theorem Subgroup.iSup_induction' {G : Type u_2} [Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop} (hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) (h1 : C 1 ⋯) (hmul : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x * y) ⋯) {x : G} (hx : x ∈ ⨆ (i : ι), S i) :
C x hx

A dependent version of Subgroup.iSup_induction.

source
theorem AddSubgroup.iSup_induction' {G : Type u_2} [AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop} (hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) (h1 : C 0 ⋯) (hadd : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x + y) ⋯) {x : G} (hx : x ∈ ⨆ (i : ι), S i) :
C x hx

A dependent version of AddSubgroup.iSup_induction.

source
theorem Subgroup.closure_mul_le {G : Type u_2} [Group G] (S T : Set G) :
closure (S * T) ≤ closure S ⊔ closure T
source
theorem AddSubgroup.closure_add_le {G : Type u_2} [AddGroup G] (S T : Set G) :
closure (S + T) ≤ closure S ⊔ closure T
source
theorem Subgroup.closure_pow_le {G : Type u_2} [Group G] {s : Set G} {n : ℕ} :
closure (s ^ n) ≤ closure s
source
theorem AddSubgroup.closure_nsmul_le {G : Type u_2} [AddGroup G] {s : Set G} {n : ℕ} :
closure (n • s) ≤ closure s
source
theorem Subgroup.closure_pow {G : Type u_2} [Group G] {s : Set G} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) :
closure (s ^ n) = closure s
source
theorem AddSubgroup.closure_nsmul {G : Type u_2} [AddGroup G] {s : Set G} {n : ℕ} (hs : 0 ∈ s) (hn : n ≠ 0) :
closure (n • s) = closure s
source
theorem Subgroup.sup_eq_closure_mul {G : Type u_2} [Group G] (H K : Subgroup G) :
H ⊔ K = closure (↑H * ↑K)
source
theorem AddSubgroup.sup_eq_closure_add {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) :
H ⊔ K = closure (↑H + ↑K)
source
theorem Subgroup.set_mul_normalizer_comm {G : Type u_2} [Group G] (S : Set G) (N : Subgroup G) (hLE : S ⊆ ↑N.normalizer) :
S * ↑N = ↑N * S
source
theorem AddSubgroup.set_add_normalizer_comm {G : Type u_2} [AddGroup G] (S : Set G) (N : AddSubgroup G) (hLE : S ⊆ ↑N.normalizer) :
S + ↑N = ↑N + S
source
theorem Subgroup.set_mul_normal_comm {G : Type u_2} [Group G] (S : Set G) (N : Subgroup G) [hN : N.Normal] :
S * ↑N = ↑N * S
source
theorem AddSubgroup.set_add_normal_comm {G : Type u_2} [AddGroup G] (S : Set G) (N : AddSubgroup G) [hN : N.Normal] :
S + ↑N = ↑N + S
source
theorem Subgroup.coe_mul_of_left_le_normalizer_right {G : Type u_2} [Group G] (H N : Subgroup G) (hLE : H ≤ N.normalizer) :
↑(H ⊔ N) = ↑H * ↑N

The carrier of H ⊔ N is just ↑H * ↑N (pointwise set product) when H is a subgroup of the normalizer of N in G.

source
theorem AddSubgroup.coe_add_of_left_le_normalizer_right {G : Type u_2} [AddGroup G] (H N : AddSubgroup G) (hLE : H ≤ N.normalizer) :
↑(H ⊔ N) = ↑H + ↑N

The carrier of H ⊔ N is just ↑H + ↑N (pointwise set addition) when H is a subgroup of the normalizer of N in G.

source
theorem Subgroup.coe_mul_of_right_le_normalizer_left {G : Type u_2} [Group G] (N H : Subgroup G) (hLE : H ≤ N.normalizer) :
↑(N ⊔ H) = ↑N * ↑H

The carrier of N ⊔ H is just ↑N * ↑H (pointwise set product) when H is a subgroup of the normalizer of N in G.

source
theorem AddSubgroup.coe_add_of_right_le_normalizer_left {G : Type u_2} [AddGroup G] (N H : AddSubgroup G) (hLE : H ≤ N.normalizer) :
↑(N ⊔ H) = ↑N + ↑H

The carrier of N ⊔ H is just ↑N + ↑H (pointwise set addition) when H is a subgroup of the normalizer of N in G.

source
theorem Subgroup.mul_normal {G : Type u_2} [Group G] (H N : Subgroup G) [hN : N.Normal] :
↑(H ⊔ N) = ↑H * ↑N

The carrier of H ⊔ N is just ↑H * ↑N (pointwise set product) when N is normal.

source
theorem AddSubgroup.add_normal {G : Type u_2} [AddGroup G] (H N : AddSubgroup G) [hN : N.Normal] :
↑(H ⊔ N) = ↑H + ↑N

The carrier of H ⊔ N is just ↑H + ↑N (pointwise set addition) when N is normal.

source
theorem Subgroup.normal_mul {G : Type u_2} [Group G] (N H : Subgroup G) [N.Normal] :
↑(N ⊔ H) = ↑N * ↑H

The carrier of N ⊔ H is just ↑N * ↑H (pointwise set product) when N is normal.

source
theorem AddSubgroup.normal_add {G : Type u_2} [AddGroup G] (N H : AddSubgroup G) [N.Normal] :
↑(N ⊔ H) = ↑N + ↑H

The carrier of N ⊔ H is just ↑N + ↑H (pointwise set addition) when N is normal.

source
theorem Subgroup.mul_inf_assoc {G : Type u_2} [Group G] (A B C : Subgroup G) (h : A ≤ C) :
↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C
source
theorem AddSubgroup.add_inf_assoc {G : Type u_2} [AddGroup G] (A B C : AddSubgroup G) (h : A ≤ C) :
↑A + ↑(B ⊓ C) = (↑A + ↑B) ∩ ↑C
source
theorem Subgroup.inf_mul_assoc {G : Type u_2} [Group G] (A B C : Subgroup G) (h : C ≤ A) :
↑(A ⊓ B) * ↑C = ↑A ∩ (↑B * ↑C)
source
theorem AddSubgroup.inf_add_assoc {G : Type u_2} [AddGroup G] (A B C : AddSubgroup G) (h : C ≤ A) :
↑(A ⊓ B) + ↑C = ↑A ∩ (↑B + ↑C)
source
instance Subgroup.sup_normal {G : Type u_2} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] :
(H ⊔ K).Normal
source
instance AddSubgroup.sup_normal {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] :
(H ⊔ K).Normal
source
theorem Subgroup.smul_mem_of_mem_closure_of_mem {G : Type u_2} [Group G] {X : Type u_5} [MulAction G X] {s : Set G} {t : Set X} (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t) {g : G} (hg : g ∈ closure s) {x : X} (hx : x ∈ t) :
g • x ∈ t
source
theorem AddSubgroup.vadd_mem_of_mem_closure_of_mem {G : Type u_2} [AddGroup G] {X : Type u_5} [AddAction G X] {s : Set G} {t : Set X} (hs : ∀ g ∈ s, -g ∈ s) (hst : ∀ g ∈ s, ∀ x ∈ t, g +ᵥ x ∈ t) {g : G} (hg : g ∈ closure s) {x : X} (hx : x ∈ t) :
g +ᵥ x ∈ t
source
theorem Subgroup.smul_opposite_image_mul_preimage' {G : Type u_2} [Group G] (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
(fun (y : G) => h • y) '' ((fun (x : G) => g * x) ⁻¹' s) = (fun (x : G) => g * x) ⁻¹' ((fun (y : G) => h • y) '' s)
source
theorem AddSubgroup.vadd_opposite_image_add_preimage' {G : Type u_2} [AddGroup G] (g : G) (h : Gᵃᵒᵖ) (s : Set G) :
(fun (y : G) => h +ᵥ y) '' ((fun (x : G) => g + x) ⁻¹' s) = (fun (x : G) => g + x) ⁻¹' ((fun (y : G) => h +ᵥ y) '' s)
source
theorem Subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [Group G] {H : Subgroup G} (g : G) (h : ↥H.op) (s : Set G) :
(fun (y : G) => h • y) '' ((fun (x : G) => g * x) ⁻¹' s) = (fun (x : G) => g * x) ⁻¹' ((fun (y : G) => h • y) '' s)
source
theorem AddSubgroup.vadd_opposite_image_add_preimage {G : Type u_2} [AddGroup G] {H : AddSubgroup G} (g : G) (h : ↥H.op) (s : Set G) :
(fun (y : G) => h +ᵥ y) '' ((fun (x : G) => g + x) ⁻¹' s) = (fun (x : G) => g + x) ⁻¹' ((fun (y : G) => h +ᵥ y) '' s)

Pointwise action #

source
def Subgroup.pointwiseMulAction {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] :
MulAction α (Subgroup G)

The action on a subgroup corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Equations
Instances For
    source
    theorem Subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] {a : α} (S : Subgroup G) :
    a • S = map ((MulDistribMulAction.toMonoidEnd α G) a) S
    source
    @[simp]
    theorem Subgroup.coe_pointwise_smul {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (S : Subgroup G) :
    ↑(a • S) = a • ↑S
    source
    @[simp]
    theorem Subgroup.pointwise_smul_toSubmonoid {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (S : Subgroup G) :
    (a • S).toSubmonoid = a • S.toSubmonoid
    source
    theorem Subgroup.smul_mem_pointwise_smul {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (m : G) (a : α) (S : Subgroup G) :
    m ∈ S → a • m ∈ a • S
    source
    instance Subgroup.instCovariantClassHSMulLe {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] :
    CovariantClass α (Subgroup G) HSMul.hSMul LE.le
    source
    theorem Subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (m : G) (a : α) (S : Subgroup G) :
    m ∈ a • S ↔ ∃ s ∈ S, a • s = m
    source
    @[simp]
    theorem Subgroup.smul_bot {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) :
    a • ⊥ = ⊥
    source
    theorem Subgroup.smul_sup {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (S T : Subgroup G) :
    a • (S ⊔ T) = a • S ⊔ a • T
    source
    theorem Subgroup.smul_closure {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (s : Set G) :
    a • closure s = closure (a • s)
    source
    instance Subgroup.pointwise_isCentralScalar {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] [MulDistribMulAction αᵐᵒᵖ G] [IsCentralScalar α G] :
    IsCentralScalar α (Subgroup G)
    source
    theorem Subgroup.conj_smul_le_of_le {G : Type u_2} [Group G] {P H : Subgroup G} (hP : P ≤ H) (h : ↥H) :
    MulAut.conj ↑h • P ≤ H
    source
    theorem Subgroup.conj_smul_subgroupOf {G : Type u_2} [Group G] {P H : Subgroup G} (hP : P ≤ H) (h : ↥H) :
    MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H
    source
    @[simp]
    theorem Subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S : Subgroup G} {x : G} :
    a • x ∈ a • S ↔ x ∈ S
    source
    theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S : Subgroup G} {x : G} :
    x ∈ a • S ↔ a⁻¹ • x ∈ S
    source
    theorem Subgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S : Subgroup G} {x : G} :
    x ∈ a⁻¹ • S ↔ a • x ∈ S
    source
    @[simp]
    theorem Subgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S T : Subgroup G} :
    a • S ≤ a • T ↔ S ≤ T
    source
    theorem Subgroup.pointwise_smul_subset_iff {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S T : Subgroup G} :
    a • S ≤ T ↔ S ≤ a⁻¹ • T
    source
    theorem Subgroup.subset_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] {a : α} {S T : Subgroup G} :
    S ≤ a • T ↔ a⁻¹ • S ≤ T
    source
    @[simp]
    theorem Subgroup.smul_inf {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (S T : Subgroup G) :
    a • (S ⊓ T) = a • S ⊓ a • T
    source
    def Subgroup.equivSMul {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) :
    ↥H ≃* ↥(a • H)

    Applying a MulDistribMulAction results in an isomorphic subgroup

    Equations
    Instances For
      source
      @[simp]
      theorem Subgroup.equivSMul_symm_apply_coe {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) (y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)) :
      ↑((equivSMul a H).symm y) = a⁻¹ • ↑y
      source
      @[simp]
      theorem Subgroup.equivSMul_apply_coe {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) (x : ↑↑H.toSubmonoid) :
      ↑((equivSMul a H) x) = a • ↑x
      source
      theorem Subgroup.subgroup_mul_singleton {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h ∈ H) :
      ↑H * {h} = ↑H
      source
      theorem Subgroup.singleton_mul_subgroup {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h ∈ H) :
      {h} * ↑H = ↑H
      source
      theorem Subgroup.Normal.conjAct {G : Type u_2} [Group G] {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) :
      g • H = H
      source
      @[simp]
      theorem Subgroup.Normal.conj_smul_eq_self {G : Type u_2} [Group G] (g : G) (H : Subgroup G) [h : H.Normal] :
      MulAut.conj g • H = H
      source
      theorem Subgroup.Normal.of_conjugate_fixed {G : Type u_2} [Group G] {H : Subgroup G} (h : ∀ (g : G), MulAut.conj g • H = H) :
      H.Normal
      source
      theorem Subgroup.normalCore_eq_iInf_conjAct {G : Type u_2} [Group G] (H : Subgroup G) :
      H.normalCore = ⨅ (g : ConjAct G), g • H
      source
      theorem Subgroup.conjAct_pointwise_smul_iff {G : Type u_2} [Group G] {H : Subgroup G} {g : G} :
      ConjAct.toConjAct g • H = H ↔ g ∈ H.normalizer
      source
      theorem Subgroup.conjAct_pointwise_smul_eq_self {G : Type u_2} [Group G] {H : Subgroup G} {g : G} (hg : g ∈ H.normalizer) :
      ConjAct.toConjAct g • H = H