Documentation

Mathlib.Algebra.GroupWithZero.Subgroup

Subgroups in a group with zero #

@[simp]

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

a • x ∈ a • S ↔ x ∈ S

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

x ∈ a • S ↔ a⁻¹ • x ∈ S

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

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

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

a • S ≤ a • T ↔ S ≤ T

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

a • S ≤ T ↔ S ≤ a⁻¹ • T

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

S ≤ a • T ↔ a⁻¹ • S ≤ T

def AddSubgroup.pointwiseMulAction {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] :

MulAction M (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 = { smul := fun (a : M) (S : AddSubgroup A) => AddSubgroup.map ((DistribMulAction.toAddMonoidEnd M A) a) S, one_smul := ⋯, mul_smul := ⋯ }

Instances For

theorem AddSubgroup.pointwise_smul_def {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] {a : M} (S : AddSubgroup A) :

a • S = map ((DistribMulAction.toAddMonoidEnd M A) a) S

@[simp]

theorem AddSubgroup.coe_pointwise_smul {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (a : M) (S : AddSubgroup A) :

↑(a • S) = a • ↑S

@[simp]

theorem AddSubgroup.pointwise_smul_toAddSubmonoid {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (a : M) (S : AddSubgroup A) :

(a • S).toAddSubmonoid = a • S.toAddSubmonoid

theorem AddSubgroup.smul_mem_pointwise_smul {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (m : A) (a : M) (S : AddSubgroup A) :

m ∈ S → a • m ∈ a • S

theorem AddSubgroup.mem_smul_pointwise_iff_exists {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (m : A) (a : M) (S : AddSubgroup A) :

m ∈ a • S ↔ ∃ s ∈ S, a • s = m

instance AddSubgroup.pointwise_isCentralScalar {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] [DistribMulAction Mᵐᵒᵖ A] [IsCentralScalar M A] :

IsCentralScalar M (AddSubgroup A)

@[simp]

theorem AddSubgroup.smul_mem_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S : AddSubgroup A} {a : G} {x : A} :

a • x ∈ a • S ↔ x ∈ S

theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S : AddSubgroup A} {a : G} {x : A} :

x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem AddSubgroup.mem_inv_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S : AddSubgroup A} {a : G} {x : A} :

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S T : AddSubgroup A} {a : G} :

a • S ≤ a • T ↔ S ≤ T

theorem AddSubgroup.pointwise_smul_le_iff {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S T : AddSubgroup A} {a : G} :

a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem AddSubgroup.le_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [Group G] [AddGroup A] [DistribMulAction G A] {S T : AddSubgroup A} {a : G} :

S ≤ a • T ↔ a⁻¹ • S ≤ T

@[simp]

theorem AddSubgroup.smul_mem_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) :

a • x ∈ a • S ↔ x ∈ S

theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) :

x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem AddSubgroup.mem_inv_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubgroup A) (x : A) :

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {S T : AddSubgroup A} {a : G₀} (ha : a ≠ 0) :

a • S ≤ a • T ↔ S ≤ T

theorem AddSubgroup.pointwise_smul_le_iff₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {S T : AddSubgroup A} {a : G₀} (ha : a ≠ 0) :

a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem AddSubgroup.le_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [GroupWithZero G₀] [AddGroup A] [DistribMulAction G₀ A] {S T : AddSubgroup A} {a : G₀} (ha : a ≠ 0) :

S ≤ a • T ↔ a⁻¹ • S ≤ T