mathlib3 documentation

group_theory.subgroup.pointwise

Pointwise instances on subgroup and add_subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

Implementation notes #

The pointwise section of this file is almost identical to group_theory/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} [has_involutive_inv G] [set_like S G] [inv_mem_class S G] {H : S} :
(↑H)⁻¹ = ↑H
source
@[simp]
theorem neg_coe_set {G : Type u_2} {S : Type u_4} [has_involutive_neg G] [set_like S G] [neg_mem_class S G] {H : S} :
-↑H = ↑H
source
@[simp]
theorem subgroup.inv_subset_closure {G : Type u_2} [group G] (S : set G) :
S⁻¹ ⊆ ↑(subgroup.closure S)
source
@[simp]
theorem add_subgroup.neg_subset_closure {G : Type u_2} [add_group G] (S : set G) :
-S ⊆ ↑(add_subgroup.closure S)
source
theorem add_subgroup.closure_to_add_submonoid {G : Type u_2} [add_group G] (S : set G) :
(add_subgroup.closure S).to_add_submonoid = add_submonoid.closure (S ∪ -S)
source
theorem subgroup.closure_to_submonoid {G : Type u_2} [group G] (S : set G) :
(subgroup.closure S).to_submonoid = submonoid.closure (S ∪ S⁻¹)
source
theorem add_subgroup.closure_induction_left {G : Type u_2} [add_group G] {s : set G} {p : G → Prop} {x : G} (h : x ∈ add_subgroup.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.

source
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.

source
theorem add_subgroup.closure_induction_right {G : Type u_2} [add_group G] {s : set G} {p : G → Prop} {x : G} (h : x ∈ add_subgroup.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.

source
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.

source
@[simp]
theorem subgroup.closure_inv {G : Type u_2} [group G] (s : set G) :
subgroup.closure s⁻¹ = subgroup.closure s
source
@[simp]
theorem add_subgroup.closure_neg {G : Type u_2} [add_group G] (s : set G) :
add_subgroup.closure (-s) = add_subgroup.closure s
source
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.

source
theorem add_subgroup.closure_induction'' {G : Type u_2} [add_group G] {s : set G} {p : G → Prop} {x : G} (h : x ∈ add_subgroup.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.

source
theorem add_subgroup.supr_induction {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → add_subgroup 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.

source
theorem subgroup.supr_induction {G : Type u_2} [group G] {ι : Sort u_1} (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.

source
theorem subgroup.supr_induction' {G : Type u_2} [group G] {ι : Sort u_1} (S : ι → subgroup G) {C : Π (x : G), (x ∈ ⨆ (i : ι), S i) → Prop} (hp : ∀ (i : ι) (x : G) (H : 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.supr_induction.

source
theorem add_subgroup.supr_induction' {G : Type u_2} [add_group G] {ι : Sort u_1} (S : ι → add_subgroup G) {C : Π (x : G), (x ∈ ⨆ (i : ι), S i) → Prop} (hp : ∀ (i : ι) (x : G) (H : 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 add_subgroup.supr_induction.

source
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
source
theorem add_subgroup.closure_add_le {G : Type u_2} [add_group G] (S T : set G) :
add_subgroup.closure (S + T) ≤ add_subgroup.closure S ⊔ add_subgroup.closure T
source
theorem subgroup.sup_eq_closure {G : Type u_2} [group G] (H K : subgroup G) :
H ⊔ K = subgroup.closure (↑H * ↑K)
source
theorem add_subgroup.sup_eq_closure {G : Type u_2} [add_group G] (H K : add_subgroup G) :
H ⊔ K = add_subgroup.closure (↑H + ↑K)
source
theorem add_subgroup.add_normal {G : Type u_2} [add_group G] (H N : add_subgroup G) [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.mul_normal {G : Type u_2} [group G] (H N : subgroup G) [N.normal] :
↑(H ⊔ N) = ↑H * ↑N

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

source
theorem add_subgroup.normal_add {G : Type u_2} [add_group G] (N H : add_subgroup 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.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 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 add_subgroup.add_inf_assoc {G : Type u_2} [add_group G] (A B C : add_subgroup 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 add_subgroup.inf_add_assoc {G : Type u_2} [add_group G] (A B C : add_subgroup G) (h : C ≤ A) :
↑(A ⊓ B) + ↑C = ↑A ⊓ (↑B + ↑C)
source
@[protected, instance]
def subgroup.sup_normal {G : Type u_2} [group G] (H K : subgroup G) [hH : H.normal] [hK : K.normal] :
(H ⊔ K).normal
source
theorem subgroup.smul_opposite_image_mul_preimage {G : Type u_2} [group G] {H : subgroup G} (g : G) (h : ↥(⇑subgroup.opposite H)) (s : set G) :
(λ (y : G), h • y) '' (has_mul.mul g ⁻¹' s) = has_mul.mul g ⁻¹' ((λ (y : G), h • y) '' s)
source
theorem add_subgroup.vadd_opposite_image_add_preimage {G : Type u_2} [add_group G] {H : add_subgroup G} (g : G) (h : ↥(⇑add_subgroup.opposite H)) (s : set G) :
(λ (y : G), h +ᵥ y) '' (has_add.add g ⁻¹' s) = has_add.add g ⁻¹' ((λ (y : G), h +ᵥ y) '' s)

Pointwise action #

source
@[protected]
def subgroup.pointwise_mul_action {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] :
mul_action α (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
source
theorem subgroup.pointwise_smul_def {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] {a : α} (S : subgroup G) :
a • S = subgroup.map (⇑(mul_distrib_mul_action.to_monoid_End α G) a) S
source
@[simp]
theorem subgroup.coe_pointwise_smul {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (S : subgroup G) :
↑(a • S) = a • ↑S
source
@[simp]
theorem subgroup.pointwise_smul_to_submonoid {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) (S : subgroup G) :
(a • S).to_submonoid = a • S.to_submonoid
source
theorem subgroup.smul_mem_pointwise_smul {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (m : G) (a : α) (S : subgroup G) :
m ∈ S → a • m ∈ a • S
source
theorem subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (m : G) (a : α) (S : subgroup G) :
m ∈ a • S ↔ ∃ (s : G), s ∈ S ∧ a • s = m
source
@[simp]
theorem subgroup.smul_bot {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] (a : α) :
a • ⊥ = ⊥
source
theorem subgroup.smul_sup {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α G] (a : α) (s : set G) :
a • subgroup.closure s = subgroup.closure (a • s)
source
@[protected, instance]
def subgroup.pointwise_central_scalar {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] [mul_distrib_mul_action αᵐᵒᵖ G] [is_central_scalar α G] :
is_central_scalar α (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) :
⇑mul_aut.conj ↑h • P ≤ H
source
theorem subgroup.conj_smul_subgroup_of {G : Type u_2} [group G] {P H : subgroup G} (hP : P ≤ H) (h : ↥H) :
⇑mul_aut.conj h • P.subgroup_of H = (⇑mul_aut.conj ↑h • P).subgroup_of H
source
@[simp]
theorem subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α 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 α] [mul_distrib_mul_action α G] (a : α) (S T : subgroup G) :
a • (S ⊓ T) = a • S ⊓ a • T
source
@[simp]
theorem subgroup.equiv_smul_apply_coe {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) (ᾰ : ↥↑(H.to_submonoid)) :
↑(⇑(subgroup.equiv_smul a H) ᾰ) = a • ↑ᾰ
source
def subgroup.equiv_smul {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) :
↥H ≃* ↥(a • H)

Applying a mul_distrib_mul_action results in an isomorphic subgroup

Equations
source
@[simp]
theorem subgroup.equiv_smul_symm_apply_coe {α : Type u_1} {G : Type u_2} [group G] [group α] [mul_distrib_mul_action α G] (a : α) (H : subgroup G) (ᾰ : ↥(⇑↑(mul_distrib_mul_action.to_mul_equiv G a) '' ↑(H.to_submonoid))) :
↑(⇑((subgroup.equiv_smul a H).symm) ᾰ) = ⇑(↑(mul_distrib_mul_action.to_mul_equiv G a).symm) ↑ᾰ
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.conj_act {G : Type u_1} [group G] {H : subgroup G} (hH : H.normal) (g : conj_act G) :
g • H = H
source
@[simp]
theorem subgroup.smul_normal {G : Type u_2} [group G] (g : G) (H : subgroup G) [h : H.normal] :
⇑mul_aut.conj g • H = H
source
@[simp]
theorem subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) (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_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) (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_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) (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_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) {S T : subgroup G} :
a • S ≤ a • T ↔ S ≤ T
source
theorem subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) {S T : subgroup G} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {G : Type u_2} [group G] [group_with_zero α] [mul_distrib_mul_action α G] {a : α} (ha : a ≠ 0) {S T : subgroup G} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
@[protected]
def add_subgroup.pointwise_mul_action {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] :
mul_action α (add_subgroup 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
source
@[simp]
theorem add_subgroup.coe_pointwise_smul {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_subgroup A) :
↑(a • S) = a • ↑S
source
@[simp]
theorem add_subgroup.pointwise_smul_to_add_submonoid {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_subgroup A) :
(a • S).to_add_submonoid = a • S.to_add_submonoid
source
theorem add_subgroup.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_subgroup A) :
m ∈ S → a • m ∈ a • S
source
theorem add_subgroup.mem_smul_pointwise_iff_exists {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_subgroup A) :
m ∈ a • S ↔ ∃ (s : A), s ∈ S ∧ a • s = m
source
@[protected, instance]
def add_subgroup.pointwise_central_scalar {α : Type u_1} {A : Type u_3} [add_group A] [monoid α] [distrib_mul_action α A] [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
is_central_scalar α (add_subgroup A)
source
@[simp]
theorem add_subgroup.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
a • x ∈ a • S ↔ x ∈ S
source
theorem add_subgroup.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem add_subgroup.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S : add_subgroup A} {x : A} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem add_subgroup.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
a • S ≤ a • T ↔ S ≤ T
source
theorem add_subgroup.pointwise_smul_le_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem add_subgroup.le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_group A] [group α] [distrib_mul_action α A] {a : α} {S T : add_subgroup A} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
@[simp]
theorem add_subgroup.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_subgroup A) (x : A) :
a • x ∈ a • S ↔ x ∈ S
source
theorem add_subgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_subgroup A) (x : A) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem add_subgroup.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) (S : add_subgroup A) (x : A) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem add_subgroup.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
a • S ≤ a • T ↔ S ≤ T
source
theorem add_subgroup.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem add_subgroup.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_group A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
S ≤ a • T ↔ a⁻¹ • S ≤ T