English
Given SetLike structures and SMulMemClass, from an IsScalarTower we can define SMulMemClass on a larger type, using smul_one_smul to transfer the smul_mem property.
Русский
Учитывая структуры SetLike и SMulMemClass, из IsScalarTower можно определить SMulMemClass на большем типе, используя smul_one_smul для переноса свойств smul_mem.
LaTeX
$$$\\text{Given } (S,M,N,\\alpha)\\text{ with SetLike and SMulMemClass } \\text{IsScalarTower } M N α \\Rightarrow \\text{SMulMemClass } S M α.$$$
Lean4
/-- This can't be an instance because Lean wouldn't know how to find `N`, but we can still use
this to manually derive `SMulMemClass` on specific types. -/
@[to_additive]
theorem _root_.SMulMemClass.ofIsScalarTower (S M N α : Type*) [SetLike S α] [SMul M N] [SMul M α] [Monoid N]
[MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] : SMulMemClass S M α :=
{ smul_mem := fun m a ha => smul_one_smul N m a ▸ SMulMemClass.smul_mem _ ha }
