Theorems · Theorem · group theory

SMulMemClass.ofIsScalarTower

∀ (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [inst : SetLike S α] [inst_1 : SMul M N]
  [inst_2 : SMul M α] [inst_3 : Monoid N] [inst_4 : MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α],
  SMulMemClass S M α

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.

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction

Cited by

3 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

SetLikeSMulSMulMonoidMulActionSMulMemClassIsScalarTower