smul — Mathlib

English

If r ∈ R and x is integral over R in A, then r • x is integral over R in A, under suitable scalar tower assumptions.

Русский

Если r ∈ R, а x интегрально над R в A, то r•x интегрально над R в A при подходящих условиях каскадирования скаляров.

LaTeX

$$$IsIntegral(R,x) \Rightarrow IsIntegral(R, r\cdot x).$$$

Lean4

theorem smul {R} [CommSemiring R] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] {x : B} (r : R)
    (hx : IsIntegral S x) : IsIntegral S (r • x) :=
  .of_mem_of_fg _ hx.fg_adjoin_singleton _ <| by rw [← algebraMap_smul S]; apply Subalgebra.smul_mem;
    exact Algebra.subset_adjoin rfl

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