instIsScalarTowerRing — Mathlib

English

There is a canonical scalar-tower relation for the ring side of an algebra extension, ensuring compatibility of scalars across the extension when considering the underlying ring structures. It ensures the tower axiom holds for the ring component of an algebra extension.

Русский

Существует каноническое отношение башни скаляров для стороны кольца алгебраического расширения, обеспечивающее совместимость скаляров при рассмотрении базовых колец и сохранение аксиомы башни.

LaTeX

$$$\\text{IsScalarTower } R \\ S \\ P.Ring$$$

Lean4

instance {R₀} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ R P.Ring :=
  IsScalarTower.of_algebraMap_eq' rfl

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