Documentation

Mathlib.GroupTheory.GroupAction.Units

Group actions on and by #

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 AddUnits.instVAdd_1 {M : Type u_3} {α : Type u_5} [AddMonoid M] [VAdd M α] :
VAdd (AddUnits M) α
Equations
  • AddUnits.instVAdd_1 = { vadd := fun (m : AddUnits M) (a : α) => m +ᵥ a }
instance Units.instSMul_1 {M : Type u_3} {α : Type u_5} [Monoid M] [SMul M α] :
SMul Mˣ α
Equations
  • Units.instSMul_1 = { smul := fun (m : Mˣ) (a : α) => m a }
instance Units.instSMulZeroClass {M : Type u_3} {α : Type u_5} [Monoid M] [Zero α] [SMulZeroClass M α] :
Equations
instance Units.instDistribSMulUnits {M : Type u_3} {α : Type u_5} [Monoid M] [AddZeroClass α] [DistribSMul M α] :
Equations
instance Units.instDistribMulAction {M : Type u_3} {α : Type u_5} [Monoid M] [AddMonoid α] [DistribMulAction M α] :
Equations
  • Units.instDistribMulAction = let __spread.0 := Units.instDistribSMulUnits; DistribMulAction.mk
Equations

Action of a group G on units of M #

A stronger form of Units.mul_action'.

Equations