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 GroupTheory/Submonoid/Pointwise.lean. Where possible, try to keep them in sync.

@[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 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 AddSubgroup.neg_subset_closure {G : Type u_2} [AddGroup G] (S : Set G) : -S ⊆ ↑(AddSubgroup.closure S)

@[simp]

theorem Subgroup.inv_subset_closure {G : Type u_2} [Group G] (S : Set G) : S⁻¹ ⊆ ↑(Subgroup.closure 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_toSubmonoid {G : Type u_2} [Group G] (S : Set G) : (Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

theorem AddSubgroup.closure_induction_left {G : Type u_2} [AddGroup G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ AddSubgroup.closure s) (H1 : p 0) (Hmul : (x : G) → x ∈ s → (y : G) → p y → p (x + y)) (Hinv : (x : G) → x ∈ s → (y : G) → p y → p (-x + y)) : p x

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

theorem Subgroup.closure_induction_left {G : Type u_2} [Group G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ Subgroup.closure s) (H1 : p 1) (Hmul : (x : G) → x ∈ s → (y : G) → p y → p (x * y)) (Hinv : (x : G) → x ∈ s → (y : G) → p y → p (x⁻¹ * y)) : p x

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

theorem AddSubgroup.closure_induction_right {G : Type u_2} [AddGroup G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ AddSubgroup.closure s) (H1 : p 0) (Hmul : (x y : G) → y ∈ s → p x → p (x + y)) (Hinv : (x y : G) → y ∈ s → p x → p (x + -y)) : p x

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

theorem Subgroup.closure_induction_right {G : Type u_2} [Group G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ Subgroup.closure s) (H1 : p 1) (Hmul : (x y : G) → y ∈ s → p x → p (x * y)) (Hinv : (x y : G) → y ∈ s → p x → p (x * y⁻¹)) : p x

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

@[simp]

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

@[simp]

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

theorem AddSubgroup.closure_induction'' {G : Type u_2} [AddGroup G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ AddSubgroup.closure s) (Hk : (x : G) → x ∈ s → p x) (Hk_inv : (x : G) → x ∈ s → p (-x)) (H1 : p 0) (Hmul : (x y : G) → p x → p y → p (x + y)) : p x

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.closure_induction'' {G : Type u_2} [Group G] {s : Set G} {p : G → Prop} {x : G} (h : x ∈ Subgroup.closure s) (Hk : (x : G) → x ∈ s → p x) (Hk_inv : (x : G) → x ∈ s → p x⁻¹) (H1 : p 1) (Hmul : (x y : G) → p x → p y → p (x * y)) : p x

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.iSup_induction {G : Type u_2} [AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : G → Prop} {x : G} (hx : x ∈ ⨆ (i : ι), S i) (hp : (i : ι) → (x : G) → x ∈ S i → C x) (h1 : C 0) (hmul : (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 : G → Prop} {x : G} (hx : x ∈ ⨆ (i : ι), S i) (hp : (i : ι) → (x : G) → x ∈ S i → C x) (h1 : C 1) (hmul : (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 : (x : G) → x ∈ ⨆ (i : ι), S i → Prop} (hp : (i : ι) → (x : G) → (hx : x ∈ S i) → C x (_ : x ∈ ⨆ (i : ι), S i)) (h1 : C 0 (_ : 0 ∈ ⨆ (i : ι), S i)) (hmul : (x y : G) → (hx : x ∈ ⨆ (i : ι), S i) → (hy : y ∈ ⨆ (i : ι), S i) → C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), S i)) {x : G} (hx : x ∈ ⨆ (i : ι), S i) : C x hx

A dependent version of AddSubgroup.iSup_induction.

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 (_ : x ∈ ⨆ (i : ι), S i)) (h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)) (hmul : (x y : G) → (hx : x ∈ ⨆ (i : ι), S i) → (hy : y ∈ ⨆ (i : ι), S i) → C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)) {x : G} (hx : x ∈ ⨆ (i : ι), S i) : C x hx

A dependent version of Subgroup.iSup_induction.

abbrev AddSubgroup.closure_add_le.match_1 {G : Type u_1} [AddGroup G] (S : Set G) (T : Set G) (_x : G) (motive : _x ∈ S + T → Prop) : (x : _x ∈ S + T) → ((_s _t : G) → (hs : _s ∈ S) → (ht : _t ∈ T) → (hx : (fun x x_1 => x + x_1) _s _t = _x) → motive (_ : ∃ a b, a ∈ S ∧ b ∈ T ∧ (fun x x_1 => x + x_1) a b = _x)) → motive x

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

theorem AddSubgroup.set_add_normal_comm {G : Type u_2} [AddGroup G] (s : Set G) (N : AddSubgroup G) [hN : AddSubgroup.Normal N] : s + ↑N = ↑N + s

theorem Subgroup.set_mul_normal_comm {G : Type u_2} [Group G] (s : Set G) (N : Subgroup G) [hN : Subgroup.Normal N] : s * ↑N = ↑N * s

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

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

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

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

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

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

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

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

theorem AddSubgroup.add_inf_assoc {G : Type u_2} [AddGroup G] (A : AddSubgroup G) (B : AddSubgroup G) (C : AddSubgroup G) (h : A ≤ C) : ↑A + ↑(B ⊓ C) = (↑A + ↑B) ⊓ ↑C

theorem Subgroup.mul_inf_assoc {G : Type u_2} [Group G] (A : Subgroup G) (B : Subgroup G) (C : Subgroup G) (h : A ≤ C) : ↑A * ↑(B ⊓ C) = ↑A * ↑B ⊓ ↑C

theorem AddSubgroup.inf_add_assoc {G : Type u_2} [AddGroup G] (A : AddSubgroup G) (B : AddSubgroup G) (C : AddSubgroup G) (h : C ≤ A) : ↑(A ⊓ B) + ↑C = ↑A ⊓ (↑B + ↑C)

theorem Subgroup.inf_mul_assoc {G : Type u_2} [Group G] (A : Subgroup G) (B : Subgroup G) (C : Subgroup G) (h : C ≤ A) : ↑(A ⊓ B) * ↑C = ↑A ⊓ ↑B * ↑C

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

Equations

• @AddSubgroup.sup_normal = @AddSubgroup.sup_normal.proof_1

theorem AddSubgroup.sup_normal.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [hH : AddSubgroup.Normal H] [hK : AddSubgroup.Normal K] : AddSubgroup.Normal (H ⊔ K)

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

Equations

• @Subgroup.sup_normal = @Subgroup.sup_normal.proof_1

theorem AddSubgroup.vadd_opposite_image_add_preimage' {G : Type u_2} [AddGroup G] (g : G) (h : Gᵃᵒᵖ) (s : Set G) : (fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)

theorem Subgroup.smul_opposite_image_mul_preimage' {G : Type u_2} [Group G] (g : G) (h : Gᵐᵒᵖ) (s : Set G) : (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)

theorem AddSubgroup.vadd_opposite_image_add_preimage {G : Type u_2} [AddGroup G] {H : AddSubgroup G} (g : G) (h : { x // x ∈ AddSubgroup.op H }) (s : Set G) : (fun y => h +ᵥ y) '' ((fun x => g + x) ⁻¹' s) = (fun x => g + x) ⁻¹' ((fun y => h +ᵥ y) '' s)

theorem Subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [Group G] {H : Subgroup G} (g : G) (h : { x // x ∈ Subgroup.op H }) (s : Set G) : (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => 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

• One or more equations did not get rendered due to their size.

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

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 ∈ 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 : Subgroup G) (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

• @Subgroup.pointwise_isCentralScalar = @Subgroup.pointwise_isCentralScalar.proof_1

theorem Subgroup.conj_smul_le_of_le {G : Type u_2} [Group G] {P : Subgroup G} {H : Subgroup G} (hP : P ≤ H) (h : { x // x ∈ H }) : ↑MulAut.conj ↑h • P ≤ H

theorem Subgroup.conj_smul_subgroupOf {G : Type u_2} [Group G] {P : Subgroup G} {H : Subgroup G} (hP : P ≤ H) (h : { x // x ∈ H }) : ↑MulAut.conj h • Subgroup.subgroupOf P H = Subgroup.subgroupOf (↑MulAut.conj ↑h • P) 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 : Subgroup G} {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 : Subgroup G} {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 : Subgroup G} {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 : Subgroup G) (T : Subgroup G) : a • (S ⊓ T) = a • S ⊓ a • T

@[simp]

theorem Subgroup.equivSMul_apply_coe {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) : ∀ (a : ↑↑H.toSubmonoid), ↑(↑(Subgroup.equivSMul a H) a) = a • ↑a

@[simp]

theorem Subgroup.equivSMul_symm_apply_coe {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) : ∀ (a : ↑(↑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)), ↑(↑(MulEquiv.symm (Subgroup.equivSMul a H)) a) = a⁻¹ • ↑a

def Subgroup.equivSMul {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) : { x // x ∈ H } ≃* { x // x ∈ a • H }

Applying a MulDistribMulAction results in an isomorphic subgroup

Equations

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

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 : Subgroup.Normal H) (g : ConjAct G) : g • H = H

@[simp]

theorem Subgroup.smul_normal {G : Type u_2} [Group G] (g : G) (H : Subgroup G) [h : Subgroup.Normal H] : ↑MulAut.conj g • H = 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 : Subgroup G} {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 : Subgroup G} {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 : Subgroup G} {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

• One or more equations did not get rendered due to their size.

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

• @AddSubgroup.pointwise_isCentralScalar = @AddSubgroup.pointwise_isCentralScalar.proof_1

@[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 : AddSubgroup A} {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 : AddSubgroup A} {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 : AddSubgroup A} {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 : AddSubgroup A} {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 : AddSubgroup A} {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 : AddSubgroup A} {T : AddSubgroup A} : S ≤ a • T ↔ a⁻¹ • S ≤ T