instIsScalarTowerSubtypeMem — Mathlib

English

There is an IsScalarTower S α β for a subgroup S ≤ G, provided the ambient data G acts on α and β with a scalar tower from G, i.e., IsScalarTower G α β.

Русский

Существование IsScalarTower для подгруппы S ≤ G, если надлежащие данные дают IsScalarTower G α β.

LaTeX

$$$\text{IsScalarTower}(S, \alpha, \beta)$$$

Lean4

/-- Note that this provides `IsScalarTower S G G` which is needed by `smul_mul_assoc`. -/
@[to_additive]
instance [SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) : IsScalarTower S α β :=
  inferInstanceAs (IsScalarTower S.toSubmonoid α β)

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