isScalarTower — Mathlib

English

If S' is a Submonoid of M' and SMul α β, SMul M' α, SMul M' β, and IsScalarTower M' α β hold, then IsScalarTower (Subtype fun x => x ∈ S') α β holds.

Русский

Если S' является подмонойдом M' и выполняются условия SMul и IsScalarTower M' α β, то ограниченный по S' стек скалярности существует.

LaTeX

$$$\text{IsScalarTower } S'\, α\, β$.$$

Lean4

/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
@[to_additive]
instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') :
    IsScalarTower S α β :=
  inferInstance

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