coeff_reflect — Mathlib

English

For fixed N, revAt N is injective: if revAt N a = revAt N b then a = b.

Русский

Для фиксированного N revAt N инъективно: если revAt N a = revAt N b, то a = b.

LaTeX

$$$\\forall a,b \\in \\mathbb{N},\\; \\mathrm{revAt}(N,a)=\\mathrm{revAt}(N,b) \\Rightarrow a=b.$$$

Lean4

@[simp]
theorem coeff_reflect (N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f.coeff (revAt N i) :=
  by
  rcases f with ⟨f⟩
  simp only [reflect, coeff]
  calc
    Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by rw [revAt_invol]
    _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _

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