English
The coefficients of map f p are contained in the image of p's coefficients under f: (map f p).coeffs ⊆ image f of p.coeffs.
Русский
Коэффициенты map f p лежат в образе коэффициентов p: (map f p).coeffs ⊆ image f (p.coeffs).
LaTeX
$$$ (\\\\mathrm{map}_f p).\\\\coeffs \\\\subseteq\\\\ image f \\\\ p.\\\\coeffs $$$
Lean4
theorem coeffs_map (f : R →+* S₁) (p : MvPolynomial σ R) [DecidableEq S₁] : (map f p).coeffs ⊆ p.coeffs.image f := by
classical
induction p using induction_on'' with
| C a => aesop (add simp coeffs_C)
| mul_X p n ih => simpa
| monomial_add a s p ha hs hp
ih =>
rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
· rw [Finset.image_union, Finset.union_subset_iff]
exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
·
exact
Finset.disjoint_of_subset_left (support_map_subset _ _) <|
Finset.disjoint_of_subset_right (support_map_subset _ _) <| disjoint_support_monomial ha hs
