reflect_support — Mathlib

English

The coefficient of reflect N f at i equals f.coeff (revAt N i).

Русский

Коэффициент Reflect N f на i равен коэффициенту f при индексе revAt N i.

LaTeX

$$$\\text{coeff}(\\mathrm{reflect}\\, N\, f)\,i = f\\,\\text{coeff}(\\mathrm{revAt}\\, N\, i).$$$

Lean4

theorem reflect_support (N : ℕ) (f : R[X]) : (reflect N f).support = Finset.image (revAt N) f.support :=
  by
  rcases f with ⟨⟩
  ext1
  simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]

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