smul_mem_lifts — Mathlib

English

For any r ∈ R, if p lifts via the algebra map, then r • p lifts as well.

Русский

Пусть r ∈ R. Если p поднимается через алгебраическое отображение, то и r • p поднимается.

LaTeX

$$$ smul\_mem\_lifts\ (R\, S)\ (\text{algebraMap})\ (p)\ (r) : r \cdot p \in \mathrm{lifts}(\mathrm{algebraMap}\, R\, S) $$$

Lean4

/-- If `p` lifts and `(r : R)` then `r • p` lifts. -/
theorem smul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts (algebraMap R S)) : r • p ∈ lifts (algebraMap R S) :=
  by
  rw [mem_lifts_iff_mem_alg] at hp ⊢
  exact Subalgebra.smul_mem (mapAlg R S).range hp r

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