add_algebraMap — Mathlib

English

If f is an injective R-algebra homomorphism, then IsConjRoot R (f x) (f y) iff IsConjRoot R x y.

Русский

Если f — инъективное гомоморфизм R-алгебр, то IsConjRoot R (f x) (f y) эквивалентно IsConjRoot R x y.

LaTeX

$$$\text{IsConjRoot}(R, f(x), f(y)) \iff \text{IsConjRoot}(R, x, y) \quad\text{при } f\text{ инъективен}$$$

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 add_algebraMap {x y : S} (r : K) (h : IsConjRoot K x y) :
    IsConjRoot K (x + algebraMap K S r) (y + algebraMap K S r) := by
  rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]

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