isScalarTower_mid — Mathlib

English

The instance isScalarTower_mid states that for S' ⊆ S, IsScalarTower R (Subtype mem S' x) T holds, i.e., the tower condition holds when passing to subalgebras on the left.

Русский

Инстанс isScalarTower_mid утверждает, что для S' ⊆ S выполняется IsScalarTower R (Subtype mem S' x) T, т.е. условие башни сохраняется при переходе к подалгебрам слева.

LaTeX

$$$IsScalarTower\ R (Subtype \{ x : S' \mid x \in S'\}) T$$$

Lean4

instance isScalarTower_mid {R S T : Type*} [CommSemiring R] [Semiring S] [AddCommMonoid T] [Algebra R S] [Module R T]
    [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) : IsScalarTower R S' T :=
  ⟨fun _x y _z => smul_assoc _ (y : S) _⟩

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