isScalarTower_liftAlgebra — Mathlib

English

There is a scalar tower structure, showing that Polynomial R) X acts compatibly with RatFunc R inside L, i.e., IsScalarTower R[X] (RatFunc R) L.

Русский

Существует структура столба скаляров, так что Polynomial R[X] действует совместимо с RatFunc R внутри L.

LaTeX

$$$IsScalarTower(R[X], \ RatFunc R, L)$$$

Lean4

/-- `FractionRing.isScalarTower_liftAlgebra` specialized to `RatFunc R`. -/
instance isScalarTower_liftAlgebra : IsScalarTower R[X] (RatFunc R) L :=
  IsScalarTower.of_algebraMap_eq fun x =>
    (IsFractionRing.lift_algebraMap (FaithfulSMul.algebraMap_injective R[X] L) x).symm

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