instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy

English

There is a natural IsScalarTower: S → R/(R a) → torsionBy(R,M,a), i.e., scalar actions from S are compatible with those from R and the quotient.

Русский

Существуют естественные цепи IsScalarTower: S → R/(R a) → torsionBy(R,M,a); т. е. действия скаляров из S согласованы с действиями из R и квот.

LaTeX

$$IsScalarTower S (R/(R a)) (torsionBy(R,M,a)).$$

Lean4

instance (a : R) {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
    IsScalarTower S (R ⧸ R ∙ a) (torsionBy R M a) :=
  inferInstance

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