mathlib documentation

group_theory.submonoid.pointwise

Pointwise instances on submonoids and add_submonoids #

This file provides the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from algebra/pointwise.lean. While the statements of these lemmas are defeq, we repeat them here due to them not being syntactically equal. Before adding new lemmas here, consider if they would also apply to the action on sets.

@[instance]
def submonoid.pointwise_mul_action {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] :

The action on a submonoid corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] (a : α) (S : submonoid M) :
(a S) = a S
theorem submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_2} [monoid M] [monoid α] [mul_distrib_mul_action α M] (m : M) (a : α) (S : submonoid M) :
m Sa m a S
@[simp]
theorem submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
a x a S x S
theorem submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
x a S a⁻¹ x S
theorem submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S : submonoid M} {x : M} :
x a⁻¹ S a x S
@[simp]
theorem submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
a S a T S T
theorem submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
a S T S a⁻¹ T
theorem submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_2} [monoid M] [group α] [mul_distrib_mul_action α M] {a : α} {S T : submonoid M} :
S a T a⁻¹ S T
@[simp]
theorem submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) (S : submonoid M) (x : M) :
a x a S x S
theorem submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) (S : submonoid M) (x : M) :
x a S a⁻¹ x S
theorem submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) (S : submonoid M) (x : M) :
x a⁻¹ S a x S
@[simp]
theorem submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) {S T : submonoid M} :
a S a T S T
theorem submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) {S T : submonoid M} :
a S T S a⁻¹ T
theorem submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {M : Type u_2} [monoid M] [group_with_zero α] [mul_distrib_mul_action α M] {a : α} (ha : a 0) {S T : submonoid M} :
S a T a⁻¹ S T
@[instance]
def add_submonoid.pointwise_mul_action {α : Type u_1} {A : Type u_3} [add_monoid A] [monoid α] [distrib_mul_action α 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
@[simp]
theorem add_submonoid.coe_pointwise_smul {α : Type u_1} {A : Type u_3} [add_monoid A] [monoid α] [distrib_mul_action α A] (a : α) (S : add_submonoid A) :
(a S) = a S
theorem add_submonoid.smul_mem_pointwise_smul {α : Type u_1} {A : Type u_3} [add_monoid A] [monoid α] [distrib_mul_action α A] (m : A) (a : α) (S : add_submonoid A) :
m Sa m a S
@[simp]
theorem add_submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
a x a S x S
theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
x a S a⁻¹ x S
theorem add_submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S : add_submonoid A} {x : A} :
x a⁻¹ S a x S
@[simp]
theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
a S a T S T
theorem add_submonoid.pointwise_smul_le_iff {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
a S T S a⁻¹ T
theorem add_submonoid.le_pointwise_smul_iff {α : Type u_1} {A : Type u_3} [add_monoid A] [group α] [distrib_mul_action α A] {a : α} {S T : add_submonoid A} :
S a T a⁻¹ S T
@[simp]
theorem add_submonoid.smul_mem_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_submonoid A) (x : A) :
a x a S x S
theorem add_submonoid.mem_pointwise_smul_iff_inv_smul_mem₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_submonoid A) (x : A) :
x a S a⁻¹ x S
theorem add_submonoid.mem_inv_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) (S : add_submonoid A) (x : A) :
x a⁻¹ S a x S
@[simp]
theorem add_submonoid.pointwise_smul_le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_submonoid A} :
a S a T S T
theorem add_submonoid.pointwise_smul_le_iff₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_submonoid A} :
a S T S a⁻¹ T
theorem add_submonoid.le_pointwise_smul_iff₀ {α : Type u_1} {A : Type u_3} [add_monoid A] [group_with_zero α] [distrib_mul_action α A] {a : α} (ha : a 0) {S T : add_submonoid A} :
S a T a⁻¹ S T