instHasCoeffsSubtypeMemSubalgebraAdjoin

English

If R0 → R → S is a scalar tower and P.HasCoeffs R0, then P.HasCoeffs R1 for any R1 in the tower.

Русский

Если дана башня скаляров R0 → R → S и P.HasCoeffs R0, то P.HasCoeffs R1 для любой R1 в башне.

LaTeX

$$$\\forall R_1\\, [\\text{CommRing } R_1]\\ [\\text{Algebra } R_0 \\; R_1]\\ [\\text{Algebra } R_1 \\; R]\\ [\\text{IsScalarTower } R_0 \\; R_1 \\; R],\\ P.HasCoeffs\\, R_1$$$

Lean4

instance (s : Set R) : P.HasCoeffs (Algebra.adjoin R₀ s) :=
  HasCoeffs.of_isScalarTower R₀

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