mathlib documentation

group_theory.subgroup.pointwise

Pointwise instances on subgroup and add_subgroups #

This file provides the actions

which matches the action of mul_action_set.

These actions are available in the pointwise locale.

Implementation notes #

This file is almost identical to group_theory/submonoid/pointwise.lean. Where possible, try to keep them in sync.

@[instance]
def subgroup.pointwise_mul_action {α : Type u_1} {G : Type u_2} [group G] [monoid α] [mul_distrib_mul_action α G] :

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

This is available as an instance in the pointwise locale.

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