C_dvd_iff_map_hom_eq_zero — Mathlib

English

An element lies in the range of map precisely when its coefficients all lie in the range of f.

Русский

Элемент принадлежит диапазону map тогда и только тогда все его коэффициенты лежат в диапазоне f.

LaTeX

$$$x \in \\mathrm{range}(\\\\mathrm{map}_f) \\\\Longleftrightarrow x.\\\\coeffs \\\\subseteq \\mathrm{range}(f)$$$

Lean4

theorem C_dvd_iff_map_hom_eq_zero (q : R →+* S₁) (r : R) (hr : ∀ r' : R, q r' = 0 ↔ r ∣ r') (φ : MvPolynomial σ R) :
    C r ∣ φ ↔ map q φ = 0 := by
  rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_iff]
  simp only [coeff_map, coeff_zero, hr]

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