# Submonoids in a group with zero #

source
@[simp]
theorem Submonoid.smul_mem_pointwise_smul_iff₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) (S : Submonoid M) (x : M) :
a • x ∈ a • S ↔ x ∈ S
source
theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) (S : Submonoid M) (x : M) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem Submonoid.mem_inv_pointwise_smul_iff₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) (S : Submonoid M) (x : M) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) {S T : Submonoid M} :
a • S ≤ a • T ↔ S ≤ T
source
theorem Submonoid.pointwise_smul_le_iff₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) {S T : Submonoid M} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem Submonoid.le_pointwise_smul_iff₀ {G₀ : Type u_1} {M : Type u_3} [Monoid M] [GroupWithZero G₀] [MulDistribMulAction G₀ M] {a : G₀} (ha : a ≠ 0) {S T : Submonoid M} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
def AddSubmonoid.pointwiseMulAction {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] :
MulAction M (AddSubmonoid A)

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

This is available as an instance in the `Pointwise` locale.

Equations

- AddSubmonoid.pointwiseMulAction = { smul := fun (a : M) (S : AddSubmonoid A) => AddSubmonoid.map ((DistribMulAction.toAddMonoidEnd M A) a) S, one_smul := ⋯, mul_smul := ⋯ }

Instances For

source
@[simp]
theorem AddSubmonoid.coe_pointwise_smul {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (m : M) (S : AddSubmonoid A) :
↑(m • S) = m • ↑S
source
theorem AddSubmonoid.smul_mem_pointwise_smul {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (a : A) (m : M) (S : AddSubmonoid A) :
a ∈ S → m • a ∈ m • S
source
theorem AddSubmonoid.mem_smul_pointwise_iff_exists {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (a : A) (m : M) (S : AddSubmonoid A) :
a ∈ m • S ↔ ∃ s ∈ S, m • s = a
source
@[simp]
theorem AddSubmonoid.smul_bot {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (m : M) :
m • ⊥ = ⊥
source
theorem AddSubmonoid.smul_sup {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (m : M) (S T : AddSubmonoid A) :
m • (S ⊔ T) = m • S ⊔ m • T
source
@[simp]
theorem AddSubmonoid.smul_closure {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (m : M) (s : Set A) :
m • closure s = closure (m • s)
source
theorem AddSubmonoid.pointwise_isCentralScalar {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] [DistribMulAction M ᵐᵒᵖ A] [IsCentralScalar M A] :
IsCentralScalar M (AddSubmonoid A)
source
@[simp]
theorem AddSubmonoid.smul_mem_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S : AddSubmonoid A} {x : A} :
a • x ∈ a • S ↔ x ∈ S
source
theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S : AddSubmonoid A} {x : A} :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem AddSubmonoid.mem_inv_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S : AddSubmonoid A} {x : A} :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S T : AddSubmonoid A} :
a • S ≤ a • T ↔ S ≤ T
source
theorem AddSubmonoid.pointwise_smul_le_iff {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S T : AddSubmonoid A} :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem AddSubmonoid.le_pointwise_smul_iff {G : Type u_2} {A : Type u_4} [AddMonoid A] [Group G] [DistribMulAction G A] {a : G} {S T : AddSubmonoid A} :
S ≤ a • T ↔ a⁻¹ • S ≤ T
source
@[simp]
theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubmonoid A) (x : A) :
a • x ∈ a • S ↔ x ∈ S
source
theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubmonoid A) (x : A) :
x ∈ a • S ↔ a⁻¹ • x ∈ S
source
theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {a : G₀} (ha : a ≠ 0) (S : AddSubmonoid A) (x : A) :
x ∈ a⁻¹ • S ↔ a • x ∈ S
source
@[simp]
theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {S T : AddSubmonoid A} {a : G₀} (ha : a ≠ 0) :
a • S ≤ a • T ↔ S ≤ T
source
theorem AddSubmonoid.pointwise_smul_le_iff₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {S T : AddSubmonoid A} {a : G₀} (ha : a ≠ 0) :
a • S ≤ T ↔ S ≤ a⁻¹ • T
source
theorem AddSubmonoid.le_pointwise_smul_iff₀ {G₀ : Type u_1} {A : Type u_4} [AddMonoid A] [GroupWithZero G₀] [DistribMulAction G₀ A] {S T : AddSubmonoid A} {a : G₀} (ha : a ≠ 0) :
S ≤ a • T ↔ a⁻¹ • S ≤ T