instIsScalarTowerRing_2 — Mathlib

English

Under the same setup as the previous statement, the scalar-tower property also holds for the underlying ring of the extension, namely IsScalarTower R0 P.Ring S.

Русский

В той же конфигурации цепь скаляров выполняется и для кольца, лежащего в основе расширения: IsScalarTower R0 P.Ring S.

LaTeX

$$$IsScalarTower\\ R_0\\ P.Ring\\ S$$$

Lean4

instance {R₀} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ P.Ring S :=
  IsScalarTower.of_algebraMap_eq' <| by
    rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ←
      IsScalarTower.algebraMap_eq]

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