# Documentation

Mathlib.GroupTheory.GroupAction.Units

# Group actions on and by Mˣ#

This file provides the action of a unit on a type α, SMul Mˣ α, in the presence of SMul M α, with the obvious definition stated in Units.smul_def. This definition preserves MulAction and DistribMulAction structures too.

Additionally, a MulAction G M for some group G satisfying some additional properties admits a MulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul. These instances use a primed name.

The results are repeated for AddUnits and VAdd where relevant.

### Action of the units of M on a type α#

instance Units.instSMulUnits {M : Type u_3} {α : Type u_5} [] [SMul M α] :
SMul Mˣ α
theorem AddUnits.vadd_def {M : Type u_3} {α : Type u_5} [] [VAdd M α] (m : ) (a : α) :
m +ᵥ a = m +ᵥ a
theorem Units.smul_def {M : Type u_3} {α : Type u_5} [] [SMul M α] (m : Mˣ) (a : α) :
m a = m a
@[simp]
theorem Units.smul_isUnit {M : Type u_3} {α : Type u_5} [] [SMul M α] {m : M} (hm : ) (a : α) :
a = m a
theorem IsUnit.inv_smul {α : Type u_5} [] {a : α} (h : ) :
()⁻¹ a = 1
instance Units.instFaithfulSMulUnitsInstSMulUnits {M : Type u_3} {α : Type u_5} [] [SMul M α] [] :
m + n +ᵥ b = m +ᵥ (n +ᵥ b)
instance Units.instSMulZeroClassUnits {M : Type u_3} {α : Type u_5} [] [Zero α] [] :
instance Units.instDistribSMulUnits {M : Type u_3} {α : Type u_5} [] [] [] :
instance Units.smulCommClass_left {M : Type u_3} {N : Type u_4} {α : Type u_5} [] [SMul M α] [SMul N α] [] :
instance Units.smulCommClass_right {M : Type u_3} {N : Type u_4} {α : Type u_5} [] [SMul M α] [SMul N α] [] :
instance Units.instIsScalarTowerUnitsInstSMulUnitsInstSMulUnits {M : Type u_3} {N : Type u_4} {α : Type u_5} [] [SMul M N] [SMul M α] [SMul N α] [] :

### Action of a group G on units of M#

instance Units.mulAction' {G : Type u_1} {M : Type u_3} [] [] [] [] [] :

If an action G associates and commutes with multiplication on M, then it lifts to an action on Mˣ. Notably, this provides MulAction Mˣ Nˣ under suitable conditions.

@[simp]
theorem Units.val_smul {G : Type u_1} {M : Type u_3} [] [] [] [] [] (g : G) (m : Mˣ) :
↑(g m) = g m
@[simp]
theorem Units.smul_inv {G : Type u_1} {M : Type u_3} [] [] [] [] [] (g : G) (m : Mˣ) :

Note that this lemma exists more generally as the global smul_inv

instance Units.smulCommClass' {G : Type u_1} {H : Type u_2} {M : Type u_3} [] [] [] [] [] [] [] [] [] [] :

Transfer SMulCommClass G H M to SMulCommClass G H Mˣ

instance Units.isScalarTower' {G : Type u_1} {H : Type u_2} {M : Type u_3} [SMul G H] [] [] [] [] [] [] [] [] [] [] :

Transfer IsScalarTower G H M to IsScalarTower G H Mˣ

instance Units.isScalarTower'_left {G : Type u_1} {M : Type u_3} {α : Type u_5} [] [] [] [SMul M α] [SMul G α] [] [] [] :

Transfer IsScalarTower G M α to IsScalarTower G Mˣ α

instance Units.mulDistribMulAction' {G : Type u_1} {M : Type u_3} [] [] [] [] [] :

A stronger form of Units.mul_action'.

theorem IsUnit.smul {G : Type u_1} {M : Type u_3} [] [] [] [] [] {m : M} (g : G) (h : ) :
IsUnit (g m)