relation_mem_range_map — Mathlib

English

The relation P.relation x belongs to the image of the map MvPolynomial.map(algebraMap R0 R).

Русский

Отношение P.relation x принадлежит образу отображения MvPolynomial.map(algebraMap R0 R).

LaTeX

$$$P.relation\\,x \\in \\mathrm{Set.range}(\\mathrm{MvPolynomial.map}(\\mathrm{algebraMap}\\,R_0\\,R))$$$

Lean4

theorem relation_mem_range_map (x : σ) : P.relation x ∈ Set.range (MvPolynomial.map (algebraMap R₀ R)) :=
  by
  rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
  exact HasCoeffs.coeffs_relation_mem_range R₀ x

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