# mathlibdocumentation

group_theory.group_action.units

# Group actions on and by Mˣ#

This file provides the action of a unit on a type α, has_scalar Mˣ α, in the presence of has_scalar M α, with the obvious definition stated in units.smul_def. This definition preserves mul_action and distrib_mul_action structures too.

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

The results are repeated for add_units and has_vadd where relevant.

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

@[protected, instance]
def units.has_scalar {M : Type u_3} {α : Type u_5} [monoid M] [ α] :
α
Equations
@[protected, instance]
def add_units.has_scalar {M : Type u_3} {α : Type u_5} [add_monoid M] [ α] :
α
Equations
m +ᵥ a = m +ᵥ a
theorem units.smul_def {M : Type u_3} {α : Type u_5} [monoid M] [ α] (m : Mˣ) (a : α) :
m a = m a
@[simp]
theorem units.smul_is_unit {M : Type u_3} {α : Type u_5} [monoid M] [ α] {m : M} (hm : is_unit m) (a : α) :
hm.unit a = m a
theorem is_unit.inv_smul {α : Type u_5} [monoid α] {a : α} (h : is_unit a) :
(h.unit)⁻¹ a = 1
@[protected, instance]
def units.has_faithful_smul {M : Type u_3} {α : Type u_5} [monoid M] [ α] [ α] :
@[protected, instance]
def add_units.has_faithful_vadd {M : Type u_3} {α : Type u_5} [add_monoid M] [ α] [ α] :
@[protected, instance]
α
Equations
@[protected, instance]
def units.mul_action {M : Type u_3} {α : Type u_5} [monoid M] [ α] :
α
Equations
@[protected, instance]
def units.distrib_mul_action {M : Type u_3} {α : Type u_5} [monoid M] [add_monoid α] [ α] :
Equations
@[protected, instance]
def units.mul_distrib_mul_action {M : Type u_3} {α : Type u_5} [monoid M] [monoid α]  :
Equations
@[protected, instance]
def units.smul_comm_class_left {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid M] [ α] [ α] [ α] :
α
@[protected, instance]
def units.smul_comm_class_right {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid N] [ α] [ α] [ α] :
α
@[protected, instance]
def units.is_scalar_tower {M : Type u_3} {N : Type u_4} {α : Type u_5} [monoid M] [ N] [ α] [ α] [ α] :
α

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

@[protected, instance]
def units.mul_action' {G : Type u_1} {M : Type u_3} [group G] [monoid M] [ M] [ M] [ M] :
Mˣ

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

Equations
@[simp]
theorem units.coe_smul {G : Type u_1} {M : Type u_3} [group G] [monoid M] [ M] [ M] [ M] (g : G) (m : Mˣ) :
(g m) = g m
@[simp]
theorem units.smul_inv {G : Type u_1} {M : Type u_3} [group G] [monoid M] [ M] [ M] [ M] (g : G) (m : Mˣ) :

Note that this lemma exists more generally as the global smul_inv

@[protected, instance]
def units.smul_comm_class' {G : Type u_1} {H : Type u_2} {M : Type u_3} [group G] [group H] [monoid M] [ M] [ M] [ M] [ M] [ M] [ M] [ M] :
Mˣ

Transfer smul_comm_class G H M to smul_comm_class G H Mˣ

@[protected, instance]
def units.is_scalar_tower' {G : Type u_1} {H : Type u_2} {M : Type u_3} [ H] [group G] [group H] [monoid M] [ M] [ M] [ M] [ M] [ M] [ M] [ M] :
Mˣ

Transfer is_scalar_tower G H M to is_scalar_tower G H Mˣ

@[protected, instance]
def units.is_scalar_tower'_left {G : Type u_1} {M : Type u_3} {α : Type u_5} [group G] [monoid M] [ M] [ α] [ α] [ M] [ M] [ α] :
α

Transfer is_scalar_tower G M α to is_scalar_tower G Mˣ α

@[protected, instance]
def units.mul_distrib_mul_action' {G : Type u_1} {M : Type u_3} [group G] [monoid M] [ M] [ M] :

A stronger form of units.mul_action'.

Equations
theorem is_unit.smul {G : Type u_1} {M : Type u_3} [group G] [monoid M] [ M] [ M] [ M] {m : M} (g : G) (h : is_unit m) :
is_unit (g m)
{"ft_lang_label":"__label__en","ft_lang_prob":0.7427885,"math_prob":0.9067796,"size":1409,"snap":"2022-27-2022-33","text_gpt3_token_len":393,"char_repetition_ratio":0.17935944,"word_repetition_ratio":0.0456621,"special_character_ratio":0.24485451,"punctuation_ratio":0.15686275,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.98956275,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-06-26T07:29:43Z\",\"WARC-Record-ID\":\"<urn:uuid:40f3079b-e9f4-486a-ade7-24db659290fc>\",\"Content-Length\":\"569683\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:c6fa179c-afef-478c-abc9-74abd50c14e8>\",\"WARC-Concurrent-To\":\"<urn:uuid:676b4fb9-63da-4af2-ae6c-f46946ecd164>\",\"WARC-IP-Address\":\"185.199.111.153\",\"WARC-Target-URI\":\"https://leanprover-community.github.io/mathlib_docs/group_theory/group_action/units.html\",\"WARC-Payload-Digest\":\"sha1:X2I26D6CEDAB2GREDEU5QOAUQTPDIKRP\",\"WARC-Block-Digest\":\"sha1:O7QNXJE6X5EONPMJEKRECFR7BXFXRF4W\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-27/CC-MAIN-2022-27_segments_1656103037649.11_warc_CC-MAIN-20220626071255-20220626101255-00295.warc.gz\"}"}