lifts_iff_coeffs_subset_range — Mathlib

English

A polynomial p lies in lifts f iff the set of its coefficients is contained in the image of f.

Русский

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

LaTeX

$$$$ p \in \mathrm{lifts}(f) \iff (p.\mathrm{coeffs} : \mathrm{Set} S) \subseteq \mathrm{Set.range}( \mathrm{RingHom.instFunLike.coe} f ) $$$$

Lean4

theorem lifts_iff_coeffs_subset_range (p : S[X]) : p ∈ lifts f ↔ (p.coeffs : Set S) ⊆ Set.range f :=
  by
  rw [lifts_iff_coeff_lifts]
  constructor
  · intro h _ hc
    obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc
    exact hn ▸ h n
  · intro h n
    by_cases hn : p.coeff n = 0
    · exact ⟨0, by simp [hn]⟩
    · exact h <| coeff_mem_coeffs hn

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