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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
theorem coe_set_eq_one {G : Type u_2} [Group G] {s : Subgroup G} :
โ†‘s = 1 โ†” s = โŠฅ
source
๐Ÿ“ coverage
theorem coe_set_eq_zero {G : Type u_2} [AddGroup G] {s : AddSubgroup G} :
โ†‘s = 0 โ†” s = โŠฅ
source
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[simp]
theorem Subgroup.inv_subset_closure {G : Type u_2} [Group G] (S : Set G) :
Sโปยน โŠ† โ†‘(closure S)
source
๐Ÿ“ coverage
@[simp]
theorem AddSubgroup.neg_subset_closure {G : Type u_2} [AddGroup G] (S : Set G) :
-S โŠ† โ†‘(closure S)
source
๐Ÿ“ coverage
theorem Subgroup.closure_toSubmonoid {G : Type u_2} [Group G] (S : Set G) :
(closure S).toSubmonoid = Submonoid.closure (S โˆช Sโปยน)
source
๐Ÿ“ coverage
theorem AddSubgroup.closure_toAddSubmonoid {G : Type u_2} [AddGroup G] (S : Set G) :
(closure S).toAddSubmonoid = AddSubmonoid.closure (S โˆช -S)
source
๐Ÿ“ coverage
theorem Subgroup.toSubmonoid_zpowers {G : Type u_2} [Group G] (g : G) :
(zpowers g).toSubmonoid = Submonoid.powers g โŠ” Submonoid.powers gโปยน
source
๐Ÿ“ coverage
theorem AddSubgroup.toAddSubmonoid_zmultiples {G : Type u_2} [AddGroup G] (g : G) :
(zmultiples g).toAddSubmonoid = AddSubmonoid.multiples g โŠ” AddSubmonoid.multiples (-g)
source
๐Ÿ“ coverage
theorem Submonoid.powers_le_zpowers {G : Type u_2} [Group G] (g : G) :
powers g โ‰ค (Subgroup.zpowers g).toSubmonoid
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
@[simp]
theorem Subgroup.closure_inv {G : Type u_2} [Group G] (s : Set G) :
closure sโปยน = closure s
source
๐Ÿ“ coverage
@[simp]
theorem AddSubgroup.closure_neg {G : Type u_2} [AddGroup G] (s : Set G) :
closure (-s) = closure s
source
๐Ÿ“ coverage
@[simp]
theorem Subgroup.closure_singleton_inv {G : Type u_2} [Group G] (x : G) :
closure {xโปยน} = closure {x}
source
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
theorem Subgroup.closure_mul_le {G : Type u_2} [Group G] (S T : Set G) :
closure (S * T) โ‰ค closure S โŠ” closure T
source
๐Ÿ“ coverage
theorem AddSubgroup.closure_add_le {G : Type u_2} [AddGroup G] (S T : Set G) :
closure (S + T) โ‰ค closure S โŠ” closure T
source
๐Ÿ“ coverage
theorem Subgroup.closure_pow_le {G : Type u_2} [Group G] {s : Set G} {n : โ„•} :
closure (s ^ n) โ‰ค closure s
source
๐Ÿ“ coverage
theorem AddSubgroup.closure_nsmul_le {G : Type u_2} [AddGroup G] {s : Set G} {n : โ„•} :
closure (n โ€ข s) โ‰ค closure s
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
theorem Subgroup.sup_eq_closure_mul {G : Type u_2} [Group G] (H K : Subgroup G) :
H โŠ” K = closure (โ†‘H * โ†‘K)
source
๐Ÿ“ coverage
theorem AddSubgroup.sup_eq_closure_add {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) :
H โŠ” K = closure (โ†‘H + โ†‘K)
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
instance Subgroup.sup_normal {G : Type u_2} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] :
(H โŠ” K).Normal
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ”ธ coverage
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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      instance Subgroup.instCovariantClassHSMulLe {ฮฑ : Type u_1} {G : Type u_2} [Group G] [Monoid ฮฑ] [MulDistribMulAction ฮฑ G] :
      CovariantClass ฮฑ (Subgroup G) HSMul.hSMul LE.le
      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[simp]
      theorem Subgroup.smul_bot {ฮฑ : Type u_1} {G : Type u_2} [Group G] [Monoid ฮฑ] [MulDistribMulAction ฮฑ G] (a : ฮฑ) :
      a โ€ข โŠฅ = โŠฅ
      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      instance Subgroup.pointwise_isCentralScalar {ฮฑ : Type u_1} {G : Type u_2} [Group G] [Monoid ฮฑ] [MulDistribMulAction ฮฑ G] [MulDistribMulAction ฮฑแตแต’แต– G] [IsCentralScalar ฮฑ G] :
      IsCentralScalar ฮฑ (Subgroup G)
      source
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      theorem Subgroup.conj_smul_eq_self_of_mem {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h โˆˆ H) :
      MulAut.conj h โ€ข H = H
      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ”ธ coverage
      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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          theorem Subgroup.subgroup_mul_singleton {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h โˆˆ H) :
          โ†‘H * {h} = โ†‘H
          source
          ๐Ÿ“ coverage
          theorem Subgroup.singleton_mul_subgroup {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h โˆˆ H) :
          {h} * โ†‘H = โ†‘H
          source
          ๐Ÿ“ coverage
          theorem Subgroup.Normal.conjAct {G : Type u_2} [Group G] {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) :
          g โ€ข H = H
          source
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          theorem Subgroup.normalCore_eq_iInf_conjAct {G : Type u_2} [Group G] (H : Subgroup G) :
          H.normalCore = โจ… (g : ConjAct G), g โ€ข H
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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