Documentation

Mathlib.Algebra.GroupWithZero.Subgroup

Subgroups in a group with zero #

source
@[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
source
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
source
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
source
@[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
source
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
source
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
source
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
    Instances For
      source
      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
      source
      @[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
      source
      @[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
      source
      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
      source
      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
      source
      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)
      source
      @[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
      source
      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
      source
      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
      source
      @[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
      source
      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
      source
      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
      source
      @[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
      source
      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
      source
      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
      source
      @[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
      source
      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
      source
      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