isScalarTower' — Mathlib

English

There is a tower S → R[X] → PolynomialModule R M when S → R and M is an S-module with IsScalarTower S R M.

Русский

Существует каскадность S → R[X] → PolynomialModule R M, когда S → R и M является S-модулем с IsScalarTower S R M.

LaTeX

$$IsScalarTower S (Polynomial R) (PolynomialModule R M)$$

Lean4

instance isScalarTower' (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S R M] :
    IsScalarTower S R[X] (PolynomialModule R M) :=
  by
  haveI : IsScalarTower R R[X] (PolynomialModule R M) :=
    inferInstanceAs <| IsScalarTower R R[X] <| Module.AEval' <| Finsupp.lmapDomain M R Nat.succ
  constructor
  intro x y z
  rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]

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