theorem
AddAction.Supports.vadd'
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddGroup G]
[AddAction G α]
[AddAction G β]
{s : Set α}
{b : β}
(g : G)
(h : AddAction.Supports G s b)
:
AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
theorem
MulAction.Supports.smul'
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[Group G]
[MulAction G α]
[MulAction G β]
{s : Set α}
{b : β}
(g : G)
(h : MulAction.Supports G s b)
:
MulAction.Supports G (g • s) (g • b)