Instances of mul_semiring_action for subobjects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
These are defined in this file as semirings are not available yet where submonoid and subgroup
are defined.
Instances for subsemiring and subring are provided next to the other scalar actions instances
for those subobjects.
@[protected, instance]
def
submonoid.mul_semiring_action
{M : Type u_1}
{R : Type u_3}
[monoid M]
[semiring R]
[mul_semiring_action M R]
(H : submonoid M) :
A stronger version of submonoid.distrib_mul_action.
Equations
- H.mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul H.has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
@[protected, instance]
def
subgroup.mul_semiring_action
{G : Type u_2}
{R : Type u_3}
[group G]
[semiring R]
[mul_semiring_action G R]
(H : subgroup G) :
A stronger version of subgroup.distrib_mul_action.