ofPrime_scalar_tower — Mathlib

English

There is a scalar tower structure linking A, A.ofPrime P, and K.

Русский

Существует структура тензорного тройного кадра скаляров между A, A.ofPrime P и K.

LaTeX

$$IsScalarTower A (A.ofPrime P) K$$

Lean4

instance ofPrime_scalar_tower (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
    letI : SMul A (A.ofPrime P) := SMulZeroClass.toSMul
    IsScalarTower A (A.ofPrime P) K :=
  IsScalarTower.subalgebra' A K K (Localization.subalgebra.ofField K _ P.primeCompl_le_nonZeroDivisors)

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