subalgebra' — Mathlib

English

If R ⟶ S ⟶ A is a scalar tower and S₀ ⊆ S is an R-subalgebra, then R ⟶ S₀ ⟶ A also forms a scalar tower.

Русский

Если существует башня скаляров R ⟶ S ⟶ A и S₀ ⊆ S — R-подалгебра, то R ⟶ S₀ ⟶ A тоже образует башню скаляров.

LaTeX

$$$\text{IsScalarTower } R \, S₀ \, A$$$

Lean4

instance subalgebra' (S₀ : Subalgebra R S) : IsScalarTower R S₀ A :=
  @IsScalarTower.of_algebraMap_eq R S₀ A _ _ _ _ _ _ fun _ ↦ (IsScalarTower.algebraMap_apply R S A _ :)

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