coe_coeffs_map — Mathlib

English

The image of the coefficients under f contains the coefficients of map f p when viewed as a set.

Русский

Образ коэффициентов через f содержит коэффициенты map f p как подмножество.

LaTeX

$$$ ((map f p).coeffs : Set S_1) \\\\subseteq f \\\\circ p.coeffs $$$

Lean4

@[simp]
theorem coe_coeffs_map (f : R →+* S₁) (p : MvPolynomial σ R) : ((map f p).coeffs : Set S₁) ⊆ f '' p.coeffs := by
  classical exact mod_cast coeffs_map f p

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