instIsScalarTower — Mathlib

English

Given SMul M N, SMul M α, SMul N α and IsScalarTower M N α, we obtain IsScalarTower (Units M) N α.

Русский

При наличии SMul M N, SMul M α, SMul N α и IsScalarTower M N α получаем IsScalarTower (Units M) N α.

LaTeX

$$$ [Monoid M] [SMul M N] [SMul M \\alpha] [SMul N \\alpha] [IsScalarTower M N \\alpha] : IsScalarTower (Units M) N \\alpha$$$

Lean4

@[to_additive]
instance [Monoid M] [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mˣ N α where
  smul_assoc m n := smul_assoc (m : M) n

Похожие утверждения