mathlib documentation

group_theory.group_action.group

Group actions applied to various types of group

This file contains lemmas about smul on units, group_with_zero, and group.

source
@[simp]
theorem units.inv_smul_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :
↑u⁻¹ • ↑u • x = x

source
@[simp]
theorem units.smul_inv_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :
↑u • ↑u⁻¹ • x = x

source
def units.smul_perm_hom {α : Type u} {β : Type v} [monoid α] [mul_action α β] :
units α →* equiv.perm β

If a monoid α acts on β, then each u : units α defines a permutation of β.

Equations
source
@[simp]
theorem units.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) {x y : β} :
↑u • x = ↑u • y ↔ x = y

source
theorem units.smul_eq_iff_eq_inv_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) {x y : β} :
↑u • x = y ↔ x = ↑u⁻¹ • y

source
theorem is_unit.smul_left_cancel {α : Type u} {β : Type v} [monoid α] [mul_action α β] {a : α} (ha : is_unit a) {x y : β} :
a • x = a • y ↔ x = y

source
@[simp]
theorem inv_smul_smul' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c ≠ 0) (x : β) :
c⁻¹ • c • x = x

source
@[simp]
theorem smul_inv_smul' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {c : α} (hc : c ≠ 0) (x : β) :
c • c⁻¹ • x = x

source
theorem inv_smul_eq_iff' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) {x y : β} :
a⁻¹ • x = y ↔ x = a • y

source
theorem eq_inv_smul_iff' {α : Type u} {β : Type v} [group_with_zero α] [mul_action α β] {a : α} (ha : a ≠ 0) {x y : β} :
x = a⁻¹ • y ↔ a • x = y

source
@[simp]
theorem inv_smul_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (c : α) (x : β) :
c⁻¹ • c • x = x

source
@[simp]
theorem smul_inv_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (c : α) (x : β) :
c • c⁻¹ • x = x

source
theorem inv_smul_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :
a⁻¹ • x = y ↔ x = a • y

source
theorem eq_inv_smul_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a : α} {x y : β} :
x = a⁻¹ • y ↔ a • x = y

source
def mul_action.to_perm (α : Type u) (β : Type v) [group α] [mul_action α β] :
α →* equiv.perm β

Given an action of a group α on a set β, each g : α defines a permutation of β.

Equations
source
theorem mul_action.bijective {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) :
function.bijective (λ (b : β), g • b)

source
theorem units.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (u : units α) {x : β} :
↑u • x = 0 ↔ x = 0

source
theorem units.smul_ne_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (u : units α) {x : β} :
↑u • x ≠ 0 ↔ x ≠ 0

source
@[simp]
theorem is_unit.smul_eq_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] {u : α} (hu : is_unit u) {x : β} :
u • x = 0 ↔ x = 0