instIsScalarTower — Mathlib

English

There is an IsScalarTower R S (AlgebraicClosure k) for any rings R,S with compatible algebra structures mapping into k.

Русский

Существуют условия IsScalarTower для R, S и AlgebraicClosure(k).

LaTeX

$$IsScalarTower\; R\; S\; (AlgebraicClosure(k))$$

Lean4

instance {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra S k] [Algebra R k]
    [IsScalarTower R S k] : IsScalarTower R S (AlgebraicClosure k) :=
  Ideal.Quotient.isScalarTower _ _ _

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