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.

@[simp]
theorem units.inv_smul_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :

@[simp]
theorem units.smul_inv_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] (u : units α) (x : β) :

def units.smul_perm_hom {α : Type u} {β : Type v} [monoid α] [mul_action α β] :

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

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

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

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

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

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

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

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

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

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

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

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

def mul_action.to_perm (α : Type u) (β : Type v) [group α] [mul_action α β] :

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

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

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

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

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