isScalarTower' — Mathlib

English

A generalized scalar tower instance for a secondary level H of structures up the tower.

Русский

Обобщённый инстанс скалярной башни для более высокого уровня структур в башне.

LaTeX

$$IsScalarTower S' R p$$

Lean4

@[to_additive]
instance isScalarTower' {S' : Type*} [SMul S' R] [SMul S' S] [SMul S' M] [IsScalarTower S' R M] [IsScalarTower S' S M] :
    IsScalarTower S' S p where smul_assoc s r x := Subtype.ext <| smul_assoc s r (x : M)

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