evalNegHom — Mathlib

English

The evaluation negation homomorphism is the ring homomorphism sending a power series f(X) to f(−X).

Русский

Гомоморфизм замены X на −X является кольцевым гомоморфизмом, отправляющим степенной ряд f(X) в f(−X).

LaTeX

$$$\\forall f\\in A\\llbracket X\\rrbracket,\\ \\operatorname{evalNegHom}(f) = f(-X)$$$

Lean4

/-- The ring homomorphism taking a power series `f(X)` to `f(-X)`. -/
noncomputable def evalNegHom : A⟦X⟧ →+* A⟦X⟧ :=
  rescale (-1 : A)

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