English
The support of reflect N f is the image of the support of f under revAt N.
Русский
Поддержка reflect N f равна образу поддержки f под revAt N.
LaTeX
$$$\\operatorname{support}(\\mathrm{reflect}\\, N\, f) = \\operatorname{image}(\\mathrm{revAt}(N))\\bigl( \\operatorname{support}(f) \\bigr).$$$
Lean4
/-- `reflect N f` is the polynomial such that `(reflect N f).coeff i = f.coeff (revAt N i)`.
In other words, the terms with exponent `[0, ..., N]` now have exponent `[N, ..., 0]`.
In practice, `reflect` is only used when `N` is at least as large as the degree of `f`.
Eventually, it will be used with `N` exactly equal to the degree of `f`. -/
noncomputable def reflect (N : ℕ) : R[X] → R[X]
| ⟨f⟩ => ⟨Finsupp.embDomain (revAt N) f⟩
