Pointwise instances on Subgroup and AddSubgroups

This file provides the actions

• Subgroup.pointwiseMulAction
• AddSubgroup.pointwiseMulAction

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. Where possible, try to keep them in sync.

@[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

@[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

@[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

@[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

theorem coe_set_eq_one {G : Type u_2} [Group G] {s : Subgroup G} : ↑s = 1 ↔ s = ⊥

theorem coe_set_eq_zero {G : Type u_2} [AddGroup G] {s : AddSubgroup G} : ↑s = 0 ↔ s = ⊥

@[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

@[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

@[simp]

theorem coe_mul_coe {G : Type u_2} {S : Type u_4} [SetLike S G] [DivInvMonoid G] [SubgroupClass S G] (H : S) : ↑H * ↑H = ↑H

@[simp]

theorem coe_add_coe {G : Type u_2} {S : Type u_4} [SetLike S G] [SubNegMonoid G] [AddSubgroupClass S G] (H : S) : ↑H + ↑H = ↑H

@[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

@[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

@[simp]

theorem Subgroup.inv_subset_closure {G : Type u_2} [Group G] (S : Set G) : S⁻¹ ⊆ ↑(Subgroup.closure S)

@[simp]

theorem AddSubgroup.neg_subset_closure {G : Type u_2} [AddGroup G] (S : Set G) : -S ⊆ ↑(AddSubgroup.closure S)

theorem Subgroup.closure_toSubmonoid {G : Type u_2} [Group G] (S : Set G) : (Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

theorem AddSubgroup.closure_toAddSubmonoid {G : Type u_2} [AddGroup G] (S : Set G) : (AddSubgroup.closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)

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

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

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

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

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

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

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

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

@[simp]

theorem Subgroup.closure_inv {G : Type u_2} [Group G] (s : Set G) : Subgroup.closure s⁻¹ = Subgroup.closure s

@[simp]

theorem AddSubgroup.closure_neg {G : Type u_2} [AddGroup G] (s : Set G) : AddSubgroup.closure (-s) = AddSubgroup.closure s

@[simp]

theorem Subgroup.closure_singleton_inv {G : Type u_2} [Group G] (x : G) : Subgroup.closure {x⁻¹} = Subgroup.closure {x}

@[simp]

theorem AddSubgroup.closure_singleton_neg {G : Type u_2} [AddGroup G] (x : G) : AddSubgroup.closure {-x} = AddSubgroup.closure {x}

theorem Subgroup.closure_induction'' {G : Type u_2} [Group G] {s : Set G} {p : (g : G) → g ∈ Subgroup.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 ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯) {x : G} (h : x ∈ Subgroup.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.

theorem AddSubgroup.closure_induction'' {G : Type u_2} [AddGroup G] {s : Set G} {p : (g : G) → g ∈ AddSubgroup.closure s → Prop} (mem : ∀ (x : G) (hx : x ∈ s), p x ⋯) (inv_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯) (one : p 0 ⋯) (mul : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯) {x : G} (h : x ∈ AddSubgroup.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.

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.

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) (one : C 0) (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 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.

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.

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 ⋯) (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 AddSubgroup.iSup_induction.

theorem Subgroup.closure_mul_le {G : Type u_2} [Group G] (S T : Set G) : Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T

theorem AddSubgroup.closure_add_le {G : Type u_2} [AddGroup G] (S T : Set G) : AddSubgroup.closure (S + T) ≤ AddSubgroup.closure S ⊔ AddSubgroup.closure T

theorem Subgroup.sup_eq_closure_mul {G : Type u_2} [Group G] (H K : Subgroup G) : H ⊔ K = Subgroup.closure (↑H * ↑K)

theorem AddSubgroup.sup_eq_closure_add {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) : H ⊔ K = AddSubgroup.closure (↑H + ↑K)

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

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

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.

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.

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.

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.

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

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

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)

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)

instance Subgroup.sup_normal {G : Type u_2} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal

Equations

• ⋯ = ⋯

instance AddSubgroup.sup_normal {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal

Equations

• ⋯ = ⋯

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 ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t

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 ∈ AddSubgroup.closure s) {x : X} (hx : x ∈ t) : g +ᵥ x ∈ t

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)

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)

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)

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

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

• Subgroup.pointwiseMulAction = MulAction.mk ⋯ ⋯

theorem Subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] {a : α} (S : Subgroup G) : a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S

@[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

@[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

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

instance Subgroup.instCovariantClassHSMulLe {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] : CovariantClass α (Subgroup G) HSMul.hSMul LE.le

Equations

• ⋯ = ⋯

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

@[simp]

theorem Subgroup.smul_bot {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) : a • ⊥ = ⊥

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

theorem Subgroup.smul_closure {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (s : Set G) : a • Subgroup.closure s = Subgroup.closure (a • s)

instance Subgroup.pointwise_isCentralScalar {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] [MulDistribMulAction αᵐᵒᵖ G] [IsCentralScalar α G] : IsCentralScalar α (Subgroup G)

Equations

• ⋯ = ⋯

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

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

@[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

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

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

@[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

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

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

@[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

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

• Subgroup.equivSMul a H = (MulDistribMulAction.toMulEquiv G a).subgroupMap H

@[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)) : ↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y

@[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) : ↑((Subgroup.equivSMul a H) x) = a • ↑x

theorem Subgroup.subgroup_mul_singleton {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h ∈ H) : ↑H * {h} = ↑H

theorem Subgroup.singleton_mul_subgroup {G : Type u_2} [Group G] {H : Subgroup G} {h : G} (hh : h ∈ H) : {h} * ↑H = ↑H

theorem Subgroup.Normal.conjAct {G : Type u_5} [Group G] {H : Subgroup G} (hH : H.Normal) (g : ConjAct G) : g • H = H

@[simp]

theorem Subgroup.smul_normal {G : Type u_2} [Group G] (g : G) (H : Subgroup G) [h : H.Normal] : MulAut.conj g • H = H

theorem Subgroup.normalCore_eq_iInf_conjAct {G : Type u_2} [Group G] (H : Subgroup G) : H.normalCore = ⨅ (g : ConjAct G), g • H

@[simp]

theorem Subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) (S : Subgroup G) (x : G) : a • x ∈ a • S ↔ x ∈ S

theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) (S : Subgroup G) (x : G) : x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem Subgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) (S : Subgroup G) (x : G) : x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem Subgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) {S T : Subgroup G} : a • S ≤ a • T ↔ S ≤ T

theorem Subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) {S T : Subgroup G} : a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem Subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [Group G] [GroupWithZero α] [MulDistribMulAction α G] {a : α} (ha : a ≠ 0) {S T : Subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T

def AddSubgroup.pointwiseMulAction {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] : MulAction α (AddSubgroup A)

The action on an additive subgroup corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Equations

• AddSubgroup.pointwiseMulAction = MulAction.mk ⋯ ⋯

theorem AddSubgroup.pointwise_smul_def {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] {a : α} (S : AddSubgroup A) : a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd α A) a) S

@[simp]

theorem AddSubgroup.coe_pointwise_smul {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] (a : α) (S : AddSubgroup A) : ↑(a • S) = a • ↑S

@[simp]

theorem AddSubgroup.pointwise_smul_toAddSubmonoid {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] (a : α) (S : AddSubgroup A) : (a • S).toAddSubmonoid = a • S.toAddSubmonoid

theorem AddSubgroup.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubgroup A) : m ∈ S → a • m ∈ a • S

theorem AddSubgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] (m : A) (a : α) (S : AddSubgroup A) : m ∈ a • S ↔ ∃ s ∈ S, a • s = m

instance AddSubgroup.pointwise_isCentralScalar {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] [DistribMulAction αᵐᵒᵖ A] [IsCentralScalar α A] : IsCentralScalar α (AddSubgroup A)

Equations

• ⋯ = ⋯

@[simp]

theorem AddSubgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubgroup A} {x : A} : a • x ∈ a • S ↔ x ∈ S

theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubgroup A} {x : A} : x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem AddSubgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S : AddSubgroup A} {x : A} : x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubgroup A} : a • S ≤ a • T ↔ S ≤ T

theorem AddSubgroup.pointwise_smul_le_iff {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubgroup A} : a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem AddSubgroup.le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [AddGroup A] [Group α] [DistribMulAction α A] {a : α} {S T : AddSubgroup A} : S ≤ a • T ↔ a⁻¹ • S ≤ T

@[simp]

theorem AddSubgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) : a • x ∈ a • S ↔ x ∈ S

theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) : x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem AddSubgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) : x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) {S T : AddSubgroup A} : a • S ≤ a • T ↔ S ≤ T

theorem AddSubgroup.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) {S T : AddSubgroup A} : a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem AddSubgroup.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [AddGroup A] [GroupWithZero α] [DistribMulAction α A] {a : α} (ha : a ≠ 0) {S T : AddSubgroup A} : S ≤ a • T ↔ a⁻¹ • S ≤ T

def AddSubgroup.mul {R : Type u_5} [NonUnitalNonAssocRing R] : Mul (AddSubgroup R)

For additive subgroups S and T of a ring, the product of S and T as submonoids is automatically a subgroup, which we define as the product of S and T as subgroups.

Equations

• AddSubgroup.mul = { mul := fun (M N : AddSubgroup R) => let __spread.0 := M.toAddSubmonoid * N.toAddSubmonoid; { toAddSubmonoid := __spread.0, neg_mem' := ⋯ } }

theorem AddSubgroup.mul_toAddSubmonoid {R : Type u_5} [NonUnitalNonAssocRing R] (M N : AddSubgroup R) : (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid