mem_map_range — Mathlib

English

For ring hom φ, p ∈ (mapRingHom φ).rangeS iff ∀ n, p.coeff n ∈ φ.rangeS.

Русский

Для гомоморфа φ: p ∈ (mapRingHom φ).rangeS тогда и только тогда, когда все коэффициенты p лежат в φ.rangeS.

LaTeX

$$$p \\in (\\mathrm{mapRingHom}\ \\phi).\\mathrm{rangeS} \\iff \\forall n, p.\\mathrm{coeff}(n) \\in \\phi.\\mathrm{rangeS}$$$

Lean4

theorem mem_map_range {R S : Type*} [Ring R] [Ring S] (f : R →+* S) {p : S[X]} :
    p ∈ (mapRingHom f).range ↔ ∀ n, p.coeff n ∈ f.range :=
  mem_map_rangeS f

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