eval₂_reverse_eq_zero_iff — Mathlib

English

Let i be a ring hom R → S and x ∈ S invertible. For any f ∈ R[X], we have that eval₂ i (⅟x) (reverse f) = 0 if and only if eval₂ i x f = 0.

Русский

Пусть i — кольцеобразное отображение R → S и x ∈ S обратим. Тогда для любого f ∈ R[X] выполняется equivalence: eval₂ i (⅟x) (reverse f) = 0 тогда и только тогда, когда eval₂ i x f = 0.

LaTeX

$$$$\\operatorname{eval}_2 i \\left( x^{-1} \\right) \\big( \\operatorname{reverse} f \\big) = 0 \\ \\iff \\ \\operatorname{eval}_2 i x f = 0.$$$$

Lean4

@[simp]
theorem eval₂_reverse_eq_zero_iff (i : R →+* S) (x : S) [Invertible x] (f : R[X]) :
    eval₂ i (⅟x) (reverse f) = 0 ↔ eval₂ i x f = 0 :=
  eval₂_reflect_eq_zero_iff i x _ _ le_rfl

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