instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure

English

There is a canonical IsScalarTower structure on A, (integralClosure A L), L, i.e., the scalar actions are compatible.

Русский

Существует каноническая структура IsScalarTower на A, (integralClosure A L), L; действия скаляров совместимы.

LaTeX

$$$IsScalarTower\; A ((integralClosure A L)) L$$$

Lean4

instance : IsScalarTower A ((integralClosure A L)) L :=
  IsScalarTower.subalgebra' A L L (integralClosure A L)

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