coeff_map_eq_comp — Mathlib

English

The polynomial has exactly two nonzero terms iff there exist k < m and nonzero x,y such that f = C x X^k + C y X^m.

Русский

Полином имеет ровно два ненулевых слагаемых тогда и только тогда, когда существуют k < m и ненулевые x,y такие, что f = C x X^k + C y X^m.

LaTeX

$$$#f.support = 2 \\iff \\exists k,m\\, (k < m) \\land \\exists x,y\\, (x \\neq 0) \\land (y \\neq 0) \\land f = C x X^k + C y X^m$$$

Lean4

theorem coeff_map_eq_comp (p : R[X]) (f : R →+* S) : (p.map f).coeff = f ∘ p.coeff := by ext n; exact coeff_map ..

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