lifts_iff_coeff_lifts — Mathlib

English

A polynomial p lies in lifts f iff each coefficient of p lies in the image of f.

Русский

Полином p принадлежит lifts f тогда и только тогда, когда каждый коэффициент p лежит в образе f.

LaTeX

$$$$ p \in \mathrm{lifts}(f) \iff \forall n : \mathbb{N}, \ p.\mathrm{coeff}(n) \in \mathrm{range}(\mathrm{RingHom.instFunLike.coe} f) $$$$

Lean4

theorem lifts_iff_coeff_lifts (p : S[X]) : p ∈ lifts f ↔ ∀ n : ℕ, p.coeff n ∈ Set.range f :=
  by
  rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]
  rfl

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