Pointwise monoid structures on SubMulAction #
This file provides SubMulAction.Monoid
and weaker typeclasses, which show that SubMulAction
s
inherit the same pointwise multiplications as sets.
To match Submodule.idemSemiring
, we do not put these in the Pointwise
locale.
instance
SubMulAction.instOneSubMulActionToSMul
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[One M]
:
One (SubMulAction R M)
instance
SubMulAction.instMulSubMulActionToSMul
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Mul M]
[IsScalarTower R M M]
:
Mul (SubMulAction R M)
theorem
SubMulAction.coe_mul
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Mul M]
[IsScalarTower R M M]
(p : SubMulAction R M)
(q : SubMulAction R M)
:
theorem
SubMulAction.mem_mul
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Mul M]
[IsScalarTower R M M]
{p : SubMulAction R M}
{q : SubMulAction R M}
{x : M}
:
instance
SubMulAction.mulOneClass
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[MulOneClass M]
[IsScalarTower R M M]
[SMulCommClass R M M]
:
MulOneClass (SubMulAction R M)
instance
SubMulAction.semiGroup
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Semigroup M]
[IsScalarTower R M M]
:
Semigroup (SubMulAction R M)
instance
SubMulAction.instMonoidSubMulActionToSMul
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Monoid M]
[IsScalarTower R M M]
[SMulCommClass R M M]
:
Monoid (SubMulAction R M)
theorem
SubMulAction.coe_pow
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Monoid M]
[IsScalarTower R M M]
[SMulCommClass R M M]
(p : SubMulAction R M)
{n : ℕ}
:
theorem
SubMulAction.subset_coe_pow
{R : Type u_1}
{M : Type u_2}
[Monoid R]
[MulAction R M]
[Monoid M]
[IsScalarTower R M M]
[SMulCommClass R M M]
(p : SubMulAction R M)
{n : ℕ}
: