isConjRoot_algHom_iff_of_injective

English

If y is a conjugate root of x then y + r is a conjugate root of x + r for any base element r.

Русский

Если y сопряжён к x, то y + r сопряжён к x + r для любого элемента r базового кольца.

LaTeX

$$$IsConjRoot(K, x + a, y + a)\quad\text{given } IsConjRoot(K, x, y),\; a = algebraMap(K, S)(r)$$$

Lean4

/-- A variant of `isConjRoot_algHom_iff`, only assuming `Function.Injective f`,
instead of `DivisionRing A`.
If `y` is a conjugate root of `x` and `f` is an injective `R`-algebra homomorphism, then `f y` is
a conjugate root of `f x`.
-/
theorem isConjRoot_algHom_iff_of_injective {x y : A} {f : A →ₐ[R] B} (hf : Function.Injective f) :
    IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y := by
  rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]

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