isScalarTower_left — Mathlib

English

Note that this provides IsScalarTower S R R, which is needed by smul_mul_assoc.

Русский

Замечание: это обеспечивает IsScalarTower S R R, необходимый для smul_mul_assoc.

LaTeX

$$$IsScalarTower\ S\ R\ R$$$

Lean4

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

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