sub_algebraMap — Mathlib

English

For a general AlgHom f, IsConjRoot R (f x) (f y) iff IsConjRoot R x y.

Русский

Для общего AlgHom f выполняется IsConjRoot R (f x) (f y) ⇔ IsConjRoot R x y.

LaTeX

$$$IsConjRoot(R, f(x), f(y)) \iff IsConjRoot(R, x, y)$$$

Lean4

/-- Let `r` be an element of the base ring. If `y` is a conjugate root of `x`, then `y - r` is a
conjugate root of `x - r`.
-/
theorem sub_algebraMap {x y : S} (r : K) (h : IsConjRoot K x y) :
    IsConjRoot K (x - algebraMap K S r) (y - algebraMap K S r) := by
  simpa only [sub_eq_add_neg, map_neg] using add_algebraMap (-r) h

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