Pi instances for multiplicative actions #
This file defines instances for mul_action and related structures on Pi types.
See also #
group_theory.group_action.option
group_theory.group_action.prod
group_theory.group_action.sigma
group_theory.group_action.sum
Equations
- pi.has_vadd' = {vadd := λ (s : Π (i : I), f i) (x : Π (i : I), g i) (i : I), s i +ᵥ x i}
Equations
- pi.has_smul' = {smul := λ (s : Π (i : I), f i) (x : Π (i : I), g i) (i : I), s i • x i}
If f i
has a faithful scalar action for a given i
, then so does Π i, f i
. This is
not an instance as i
cannot be inferred.
If f i
has a faithful additive action for a given i
, then
so does Π i, f i
. This is not an instance as i
cannot be inferred
Equations
- pi.add_action α = {to_has_vadd := {vadd := has_vadd.vadd pi.has_vadd}, zero_vadd := _, add_vadd := _}
Equations
- pi.mul_action α = {to_has_smul := {smul := has_smul.smul pi.has_smul}, one_smul := _, mul_smul := _}
Equations
- pi.add_action' = {to_has_vadd := {vadd := has_vadd.vadd pi.has_vadd'}, zero_vadd := _, add_vadd := _}
Equations
- pi.mul_action' = {to_has_smul := {smul := has_smul.smul pi.has_smul'}, one_smul := _, mul_smul := _}
Equations
- pi.distrib_mul_action α = {to_mul_action := {to_has_smul := mul_action.to_has_smul (pi.mul_action α), one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Equations
- pi.distrib_mul_action' = {to_mul_action := pi.mul_action' (λ (i : I), distrib_mul_action.to_mul_action), smul_add := _, smul_zero := _}
A version of pi.single_smul
for non-dependent functions. It is useful in cases Lean fails
to apply pi.single_smul
.
Equations
- pi.mul_distrib_mul_action α = {to_mul_action := {to_has_smul := mul_action.to_has_smul (pi.mul_action α), one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
Equations
- pi.mul_distrib_mul_action' = {to_mul_action := pi.mul_action' (λ (i : I), mul_distrib_mul_action.to_mul_action), smul_mul := _, smul_one := _}
Non-dependent version of pi.has_vadd
. Lean gets confused by the dependent instance
if this is not present.
Equations
Non-dependent version of pi.has_smul
. Lean gets confused by the dependent instance if this
is not present.
Equations
Non-dependent version of pi.smul_comm_class
. Lean gets confused by the dependent instance if
this is not present.
Non-dependent version of pi.vadd_comm_class
. Lean gets confused by the dependent
instance if this is not present.