instIsScalarTowerSubtypeMem — Mathlib

English

If α and β are SMul R-modules with an IsScalarTower relation and S is a Subring of R, then the induced IsScalarTower relation holds for S with the same α and β.

Русский

Пусть α, β — модули над кольцом R с отношением IsScalarTower; если S ⊆ R — подкольцо, то для той же пары α, β выполняется аналогичное отношение для S.

LaTeX

$$$IsScalarTower\; S\; \alpha\; \beta$$$

Lean4

/-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`. -/
instance [SMul α β] [SMul R α] [SMul R β] [IsScalarTower R α β] (S : Subring R) : IsScalarTower S α β :=
  inferInstanceAs (IsScalarTower S.toSubsemiring α β)

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