of_isScalarTower — Mathlib

English

If P.HasCoeffs R0 holds, then for any subset s of R, P.HasCoeffs (Algebra.adjoin R0 s).

Русский

Если выполняется P.HasCoeffs R0, то для любого множества s из R выполняется P.HasCoeffs (Algebra.adjoin R0 s).

LaTeX

$$$P.HasCoeffs\\, R_0 \\Rightarrow P.HasCoeffs\\, (\\mathrm{Algebra.adjoin}\\, R_0\\, s)$$$

Lean4

theorem of_isScalarTower {R₁ : Type*} [CommRing R₁] [Algebra R₀ R₁] [Algebra R₁ R] [IsScalarTower R₀ R₁ R]
    [Algebra R₁ S] [IsScalarTower R₁ R S] : P.HasCoeffs R₁ :=
  by
  refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
  simp [IsScalarTower.algebraMap_eq R₀ R₁ R, RingHom.coe_comp, Set.range_comp]

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