Submonoids in a group with zero

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

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

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

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

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

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

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 := ⋯ }

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

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

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

@[simp]

theorem AddSubmonoid.smul_bot {M : Type u_3} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] (m : M) : m • ⊥ = ⊥

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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