Documentation

Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise

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