mathlib3documentation

algebra.hom.group_action

Equivariant homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

• mul_action_hom M X Y, the type of equivariant functions from X to Y, where M is a monoid that acts on the types X and Y.
• distrib_mul_action_hom M A B, the type of equivariant additive monoid homomorphisms from A to B, where M is a monoid that acts on the additive monoids A and B.
• mul_semiring_action_hom M R S, the type of equivariant ring homomorphisms from R to S, where M is a monoid that acts on the rings R and S.

The above types have corresponding classes:

• smul_hom_class F M X Y states that F is a type of bundled X → Y homs preserving scalar multiplication by M
• distrib_mul_action_hom_class F M A B states that F is a type of bundled A → B homs preserving the additive monoid structure and scalar multiplication by M
• mul_semiring_action_hom_class F M R S states that F is a type of bundled R → S homs preserving the ring structure and scalar multiplication by M

Notations #

• X →[M] Y is mul_action_hom M X Y.
• A →+[M] B is distrib_mul_action_hom M A B.
• R →+*[M] S is mul_semiring_action_hom M R S.
@[nolint]
structure mul_action_hom (M' : Type u_1) (X : Type u_2) [has_smul M' X] (Y : Type u_3) [has_smul M' Y] :
Type (max u_2 u_3)

Equivariant functions.

Instances for mul_action_hom
@[class]
structure smul_hom_class (F : Type u_16) (M : out_param (Type u_17)) (X : out_param (Type u_18)) (Y : out_param (Type u_19)) [ X] [ Y] :
Type (max u_16 u_18 u_19)
• coe : F Π (a : X), (λ (_x : X), Y) a
• coe_injective' :
• map_smul : (f : F) (c : M) (x : X), f (c x) = c f x

smul_hom_class F M X Y states that F is a type of morphisms preserving scalar multiplication by M.

You should extend this class when you extend mul_action_hom.

Instances of this typeclass
Instances of other typeclasses for smul_hom_class
• smul_hom_class.has_sizeof_inst
@[nolint, instance]
def smul_hom_class.to_fun_like (F : Type u_16) (M : out_param (Type u_17)) (X : out_param (Type u_18)) (Y : out_param (Type u_19)) [ X] [ Y] [self : X Y] :
X (λ (_x : X), Y)
@[protected, instance]
def mul_action_hom.has_coe_to_fun (M' : Type u_1) (X : Type u_2) [has_smul M' X] (Y : Type u_3) [has_smul M' Y] :
has_coe_to_fun (X →[M'] Y) (λ (_x : X →[M'] Y), X Y)
Equations
@[protected, instance]
def mul_action_hom.smul_hom_class (M' : Type u_1) (X : Type u_2) [has_smul M' X] (Y : Type u_3) [has_smul M' Y] :
smul_hom_class (X →[M'] Y) M' X Y
Equations
@[protected]
theorem mul_action_hom.map_smul {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] (f : X →[M'] Y) (m : M') (x : X) :
f (m x) = m f x
@[ext]
theorem mul_action_hom.ext {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] {f g : X →[M'] Y} :
( (x : X), f x = g x) f = g
theorem mul_action_hom.ext_iff {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] {f g : X →[M'] Y} :
f = g (x : X), f x = g x
@[protected]
theorem mul_action_hom.congr_fun {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] {f g : X →[M'] Y} (h : f = g) (x : X) :
f x = g x
@[protected]
def mul_action_hom.id (M' : Type u_1) {X : Type u_2} [has_smul M' X] :
X →[M'] X

The identity map as an equivariant map.

Equations
@[simp]
theorem mul_action_hom.id_apply (M' : Type u_1) {X : Type u_2} [has_smul M' X] (x : X) :
x = x
def mul_action_hom.comp {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] {Z : Type u_4} [has_smul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) :
X →[M'] Z

Composition of two equivariant maps.

Equations
@[simp]
theorem mul_action_hom.comp_apply {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] {Z : Type u_4} [has_smul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) :
(g.comp f) x = g (f x)
@[simp]
theorem mul_action_hom.id_comp {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] (f : X →[M'] Y) :
.comp f = f
@[simp]
theorem mul_action_hom.comp_id {M' : Type u_1} {X : Type u_2} [has_smul M' X] {Y : Type u_3} [has_smul M' Y] (f : X →[M'] Y) :
f.comp = f
def mul_action_hom.inverse {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →[M] B) (g : B A) (h₁ : f) (h₂ : f) :
B →[M] A

The inverse of a bijective equivariant map is equivariant.

Equations
@[simp]
theorem mul_action_hom.inverse_to_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →[M] B) (g : B A) (h₁ : f) (h₂ : f) (ᾰ : B) :
(f.inverse g h₁ h₂) = g ᾰ
def distrib_mul_action_hom.to_mul_action_hom {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (self : A →+[M] B) :
A →[M] B

Reinterpret an equivariant additive monoid homomorphism as an equivariant function.

def distrib_mul_action_hom.to_add_monoid_hom {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (self : A →+[M] B) :
A →+ B

structure distrib_mul_action_hom (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [ A] (B : Type u_8) [add_monoid B] [ B] :
Type (max u_6 u_8)

Instances for distrib_mul_action_hom
@[class]
structure distrib_mul_action_hom_class (F : Type u_16) (M : out_param (Type u_17)) (A : out_param (Type u_18)) (B : out_param (Type u_19)) [monoid M] [add_monoid A] [add_monoid B] [ A] [ B] :
Type (max u_16 u_18 u_19)
• coe : F Π (a : A), (λ (_x : A), B) a
• coe_injective' :
• map_smul : (f : F) (c : M) (x : A), f (c x) = c f x
• map_add : (f : F) (x y : A), f (x + y) = f x + f y
• map_zero : (f : F), f 0 = 0

distrib_mul_action_hom_class F M A B states that F is a type of morphisms preserving the additive monoid structure and scalar multiplication by M.

You should extend this class when you extend distrib_mul_action_hom.

Instances of this typeclass
Instances of other typeclasses for distrib_mul_action_hom_class
• distrib_mul_action_hom_class.has_sizeof_inst
@[nolint, instance]
def distrib_mul_action_hom_class.to_add_monoid_hom_class (F : Type u_16) (M : out_param (Type u_17)) (A : out_param (Type u_18)) (B : out_param (Type u_19)) [monoid M] [add_monoid A] [add_monoid B] [ A] [ B] [self : B] :
B
@[instance]
def distrib_mul_action_hom_class.to_smul_hom_class (F : Type u_16) (M : out_param (Type u_17)) (A : out_param (Type u_18)) (B : out_param (Type u_19)) [monoid M] [add_monoid A] [add_monoid B] [ A] [ B] [self : B] :
A B
@[protected, instance]
def distrib_mul_action_hom.has_coe (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [ A] (B : Type u_8) [add_monoid B] [ B] :
has_coe (A →+[M] B) (A →+ B)
Equations
@[protected, instance]
def distrib_mul_action_hom.has_coe' (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [ A] (B : Type u_8) [add_monoid B] [ B] :
has_coe (A →+[M] B) (A →[M] B)
Equations
@[protected, instance]
def distrib_mul_action_hom.has_coe_to_fun (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [ A] (B : Type u_8) [add_monoid B] [ B] :
has_coe_to_fun (A →+[M] B) (λ (_x : A →+[M] B), A B)
Equations
@[protected, instance]
def distrib_mul_action_hom.distrib_mul_action_hom_class (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [ A] (B : Type u_8) [add_monoid B] [ B] :
M A B
Equations
@[simp]
theorem distrib_mul_action_hom.to_fun_eq_coe {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
@[norm_cast]
theorem distrib_mul_action_hom.coe_fn_coe {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
@[norm_cast]
theorem distrib_mul_action_hom.coe_fn_coe' {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
@[ext]
theorem distrib_mul_action_hom.ext {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {f g : A →+[M] B} :
( (x : A), f x = g x) f = g
theorem distrib_mul_action_hom.ext_iff {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {f g : A →+[M] B} :
f = g (x : A), f x = g x
@[protected]
theorem distrib_mul_action_hom.congr_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {f g : A →+[M] B} (h : f = g) (x : A) :
f x = g x
theorem distrib_mul_action_hom.to_mul_action_hom_injective {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {f g : A →+[M] B} (h : f = g) :
f = g
theorem distrib_mul_action_hom.to_add_monoid_hom_injective {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {f g : A →+[M] B} (h : f = g) :
f = g
@[protected]
theorem distrib_mul_action_hom.map_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
f 0 = 0
@[protected]
theorem distrib_mul_action_hom.map_add {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) (x y : A) :
f (x + y) = f x + f y
@[protected]
theorem distrib_mul_action_hom.map_neg {M : Type u_5} [monoid M] (A' : Type u_7) [add_group A'] [ A'] (B' : Type u_9) [add_group B'] [ B'] (f : A' →+[M] B') (x : A') :
f (-x) = -f x
@[protected]
theorem distrib_mul_action_hom.map_sub {M : Type u_5} [monoid M] (A' : Type u_7) [add_group A'] [ A'] (B' : Type u_9) [add_group B'] [ B'] (f : A' →+[M] B') (x y : A') :
f (x - y) = f x - f y
@[protected]
theorem distrib_mul_action_hom.map_smul {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) (m : M) (x : A) :
f (m x) = m f x
@[protected]
def distrib_mul_action_hom.id (M : Type u_5) [monoid M] {A : Type u_6} [add_monoid A] [ A] :
A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Equations
@[simp]
theorem distrib_mul_action_hom.id_apply (M : Type u_5) [monoid M] {A : Type u_6} [add_monoid A] [ A] (x : A) :
= x
@[protected, instance]
def distrib_mul_action_hom.has_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] :
Equations
@[protected, instance]
def distrib_mul_action_hom.has_one {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] :
Equations
@[simp]
theorem distrib_mul_action_hom.coe_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] :
0 = 0
@[simp]
theorem distrib_mul_action_hom.coe_one {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] :
theorem distrib_mul_action_hom.zero_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (a : A) :
0 a = 0
theorem distrib_mul_action_hom.one_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] (a : A) :
1 a = a
@[protected, instance]
def distrib_mul_action_hom.inhabited {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] :
Equations
def distrib_mul_action_hom.comp {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {C : Type u_10} [add_monoid C] [ C] (g : B →+[M] C) (f : A →+[M] B) :
A →+[M] C

Composition of two equivariant additive monoid homomorphisms.

Equations
@[simp]
theorem distrib_mul_action_hom.comp_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] {C : Type u_10} [add_monoid C] [ C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :
(g.comp f) x = g (f x)
@[simp]
theorem distrib_mul_action_hom.id_comp {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
= f
@[simp]
theorem distrib_mul_action_hom.comp_id {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) :
= f
def distrib_mul_action_hom.inverse {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) (g : B A) (h₁ : f) (h₂ : f) :
B →+[M] A

The inverse of a bijective distrib_mul_action_hom is a distrib_mul_action_hom.

Equations
@[simp]
theorem distrib_mul_action_hom.inverse_to_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [ A] {B : Type u_8} [add_monoid B] [ B] (f : A →+[M] B) (g : B A) (h₁ : f) (h₂ : f) (ᾰ : B) :
(f.inverse g h₁ h₂) = g ᾰ
@[ext]
theorem distrib_mul_action_hom.ext_ring {M' : Type u_1} {R : Type u_11} [semiring R] [add_monoid M'] [ M'] {f g : R →+[R] M'} (h : f 1 = g 1) :
f = g
theorem distrib_mul_action_hom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [semiring R] [add_monoid M'] [ M'] {f g : R →+[R] M'} :
f = g f 1 = g 1
def mul_semiring_action_hom.to_distrib_mul_action_hom {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (self : R →+*[M] S) :
R →+[M] S

Reinterpret an equivariant ring homomorphism as an equivariant additive monoid homomorphism.

def mul_semiring_action_hom.to_ring_hom {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (self : R →+*[M] S) :
R →+* S

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

@[nolint]
structure mul_semiring_action_hom (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [ R] (S : Type u_13) [semiring S] [ S] :
Type (max u_11 u_13)

Equivariant ring homomorphisms.

Instances for mul_semiring_action_hom
@[instance]
def mul_semiring_action_hom_class.to_distrib_mul_action_hom_class (F : Type u_16) (M : out_param (Type u_17)) (R : out_param (Type u_18)) (S : out_param (Type u_19)) [monoid M] [semiring R] [semiring S] [ R] [ S] [self : S] :
S
@[nolint, instance]
def mul_semiring_action_hom_class.to_ring_hom_class (F : Type u_16) (M : out_param (Type u_17)) (R : out_param (Type u_18)) (S : out_param (Type u_19)) [monoid M] [semiring R] [semiring S] [ R] [ S] [self : S] :
S
@[class]
structure mul_semiring_action_hom_class (F : Type u_16) (M : out_param (Type u_17)) (R : out_param (Type u_18)) (S : out_param (Type u_19)) [monoid M] [semiring R] [semiring S] [ R] [ S] :
Type (max u_16 u_18 u_19)
• coe : F Π (a : R), (λ (_x : R), S) a
• coe_injective' :
• map_smul : (f : F) (c : M) (x : R), f (c x) = c f x
• map_add : (f : F) (x y : R), f (x + y) = f x + f y
• map_zero : (f : F), f 0 = 0
• map_mul : (f : F) (x y : R), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1

mul_semiring_action_hom_class F M R S states that F is a type of morphisms preserving the ring structure and scalar multiplication by M.

You should extend this class when you extend mul_semiring_action_hom.

Instances of this typeclass
Instances of other typeclasses for mul_semiring_action_hom_class
• mul_semiring_action_hom_class.has_sizeof_inst
@[protected, instance]
def mul_semiring_action_hom.has_coe (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [ R] (S : Type u_13) [semiring S] [ S] :
has_coe (R →+*[M] S) (R →+* S)
Equations
@[protected, instance]
def mul_semiring_action_hom.has_coe' (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [ R] (S : Type u_13) [semiring S] [ S] :
has_coe (R →+*[M] S) (R →+[M] S)
Equations
@[protected, instance]
def mul_semiring_action_hom.has_coe_to_fun (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [ R] (S : Type u_13) [semiring S] [ S] :
has_coe_to_fun (R →+*[M] S) (λ (_x : R →+*[M] S), R S)
Equations
@[protected, instance]
def mul_semiring_action_hom.mul_semiring_action_hom_class (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [ R] (S : Type u_13) [semiring S] [ S] :
M R S
Equations
@[norm_cast]
theorem mul_semiring_action_hom.coe_fn_coe {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
@[norm_cast]
theorem mul_semiring_action_hom.coe_fn_coe' {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
@[ext]
theorem mul_semiring_action_hom.ext {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] {f g : R →+*[M] S} :
( (x : R), f x = g x) f = g
theorem mul_semiring_action_hom.ext_iff {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] {f g : R →+*[M] S} :
f = g (x : R), f x = g x
@[protected]
theorem mul_semiring_action_hom.map_zero {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
f 0 = 0
@[protected]
theorem mul_semiring_action_hom.map_add {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) (x y : R) :
f (x + y) = f x + f y
@[protected]
theorem mul_semiring_action_hom.map_neg {M : Type u_5} [monoid M] (R' : Type u_12) [ring R'] [ R'] (S' : Type u_14) [ring S'] [ S'] (f : R' →+*[M] S') (x : R') :
f (-x) = -f x
@[protected]
theorem mul_semiring_action_hom.map_sub {M : Type u_5} [monoid M] (R' : Type u_12) [ring R'] [ R'] (S' : Type u_14) [ring S'] [ S'] (f : R' →+*[M] S') (x y : R') :
f (x - y) = f x - f y
@[protected]
theorem mul_semiring_action_hom.map_one {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
f 1 = 1
@[protected]
theorem mul_semiring_action_hom.map_mul {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) (x y : R) :
f (x * y) = f x * f y
@[protected]
theorem mul_semiring_action_hom.map_smul {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) (m : M) (x : R) :
f (m x) = m f x
@[protected]
def mul_semiring_action_hom.id (M : Type u_5) [monoid M] {R : Type u_11} [semiring R] [ R] :
R →+*[M] R

The identity map as an equivariant ring homomorphism.

Equations
@[simp]
theorem mul_semiring_action_hom.id_apply (M : Type u_5) [monoid M] {R : Type u_11} [semiring R] [ R] (x : R) :
= x
def mul_semiring_action_hom.comp {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] {T : Type u_15} [semiring T] [ T] (g : S →+*[M] T) (f : R →+*[M] S) :
R →+*[M] T

Composition of two equivariant additive monoid homomorphisms.

Equations
@[simp]
theorem mul_semiring_action_hom.comp_apply {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] {T : Type u_15} [semiring T] [ T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :
(g.comp f) x = g (f x)
@[simp]
theorem mul_semiring_action_hom.id_comp {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
= f
@[simp]
theorem mul_semiring_action_hom.comp_id {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [ R] {S : Type u_13} [semiring S] [ S] (f : R →+*[M] S) :
= f