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. 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 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
@[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 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 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 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_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_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 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]
@[simp]
theorem Subgroup.inv_subset_closure {G : Type u_2} [Group G] (S : Set G) :
theorem Subgroup.closure_toSubmonoid {G : Type u_2} [Group G] (S : Set G) :
theorem AddSubgroup.closure_induction_left {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x AddSubgroup.closure sProp} (one : p 0 ) (mul_left : ∀ (x : G) (hx : x s) (y : G) (hy : y AddSubgroup.closure s), p y hyp (x + y) ) (inv_mul_cancel : ∀ (x : G) (hx : x s) (y : G) (hy : y AddSubgroup.closure s), p y hyp (-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_left {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x Subgroup.closure sProp} (one : p 1 ) (mul_left : ∀ (x : G) (hx : x s) (y : G) (hy : y Subgroup.closure s), p y hyp (x * y) ) (inv_mul_cancel : ∀ (x : G) (hx : x s) (y : G) (hy : y Subgroup.closure s), p y hyp (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_right {G : Type u_2} [AddGroup G] {s : Set G} {p : (x : G) → x AddSubgroup.closure sProp} (one : p 0 ) (mul_right : ∀ (x : G) (hx : x AddSubgroup.closure s) (y : G) (hy : y s), p x hxp (x + y) ) (mul_inv_cancel : ∀ (x : G) (hx : x AddSubgroup.closure s) (y : G) (hy : y s), p x hxp (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.

theorem Subgroup.closure_induction_right {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x Subgroup.closure sProp} (one : p 1 ) (mul_right : ∀ (x : G) (hx : x Subgroup.closure s) (y : G) (hy : y s), p x hxp (x * y) ) (mul_inv_cancel : ∀ (x : G) (hx : x Subgroup.closure s) (y : G) (hy : y s), p x hxp (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'' {G : Type u_2} [AddGroup G] {s : Set G} {p : (g : G) → g AddSubgroup.closure sProp} (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 hxp y hyp (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.closure_induction'' {G : Type u_2} [Group G] {s : Set G} {p : (g : G) → g Subgroup.closure sProp} (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 hxp y hyp (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.iSup_induction {G : Type u_2} [AddGroup G] {ι : Sort u_5} (S : ιAddSubgroup G) {C : GProp} {x : G} (hx : x ⨆ (i : ι), S i) (mem : ∀ (i : ι), xS i, C x) (one : C 0) (mul : ∀ (x y : G), C xC yC (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 : GProp} {x : G} (hx : x ⨆ (i : ι), S i) (mem : ∀ (i : ι), xS i, C x) (one : C 1) (mul : ∀ (x y : G), C xC yC (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 iProp} (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 hxC y hyC (x + y) ) {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 iProp} (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 hxC y hyC (x * y) ) {x : G} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of Subgroup.iSup_induction.

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 : N.Normal] :
s + N = N + s
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.add_normal {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (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.mul_normal {G : Type u_2} [Group G] (H : Subgroup G) (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.normal_add {G : Type u_2} [AddGroup G] (N : AddSubgroup G) (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.normal_mul {G : Type u_2} [Group G] (N : Subgroup G) (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.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 : H.Normal] [hK : K.Normal] :
(H K).Normal
Equations
  • =
instance Subgroup.sup_normal {G : Type u_2} [Group G] (H : Subgroup G) (K : Subgroup G) [hH : H.Normal] [hK : K.Normal] :
(H K).Normal
Equations
  • =
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 : gs, -g s) (hst : gs, xt, g +ᵥ x t) {g : G} (hg : g AddSubgroup.closure s) {x : X} (hx : x t) :
g +ᵥ x t
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 : gs, g⁻¹ s) (hst : gs, xt, g x t) {g : G} (hg : g Subgroup.closure s) {x : X} (hx : x t) :
g x t
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] (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] {H : AddSubgroup G} (g : G) (h : { x : Gᵃᵒᵖ // x 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 Subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [Group G] {H : Subgroup G} (g : G) (h : { x : Gᵐᵒᵖ // x 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] :

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
    theorem Subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] {a : α} (S : Subgroup G) :
    @[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 Sa 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 sS, a s = m
    @[simp]
    theorem Subgroup.smul_bot {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (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) :
    theorem Subgroup.conj_smul_le_of_le {G : Type u_2} [Group G] {P : Subgroup G} {H : Subgroup G} (hP : P H) (h : { x : G // 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 : G // x 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 : 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) (x : H.toSubmonoid) :
    ((Subgroup.equivSMul a H) x) = a x
    @[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
    def Subgroup.equivSMul {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) :
    { x : G // x H } ≃* { x : G // x a H }

    Applying a MulDistribMulAction results in an isomorphic subgroup

    Equations
    Instances For
      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
      @[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

      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
      Instances For
        theorem AddSubgroup.pointwise_smul_def {α : Type u_1} {A : Type u_3} [AddGroup A] [Monoid α] [DistribMulAction α A] {a : α} (S : AddSubgroup A) :
        @[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 Sa 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 sS, a s = m
        @[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