Group actions applied to various types of group
This file contains lemmas about smul
on units
, group_with_zero
, and group
.
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 β
.
theorem
is_unit.smul_left_cancel
{α : Type u}
{β : Type v}
[monoid α]
[mul_action α β]
{a : α}
(ha : is_unit a)
{x y : β} :
@[simp]
theorem
inv_smul_smul'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{c : α}
(hc : c ≠ 0)
(x : β) :
@[simp]
theorem
smul_inv_smul'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{c : α}
(hc : c ≠ 0)
(x : β) :
theorem
inv_smul_eq_iff'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{x y : β} :
theorem
eq_inv_smul_iff'
{α : Type u}
{β : Type v}
[group_with_zero α]
[mul_action α β]
{a : α}
(ha : a ≠ 0)
{x y : β} :
@[simp]
@[simp]
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 : β} :
theorem
units.smul_ne_zero
{α : Type u}
{β : Type v}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
(u : units α)
{x : β} :
@[simp]
theorem
is_unit.smul_eq_zero
{α : Type u}
{β : Type v}
[monoid α]
[add_monoid β]
[distrib_mul_action α β]
{u : α}
(hu : is_unit u)
{x : β} :