isConjRoot_iff_eq_algebraMap — Mathlib

English

For an element r, IsConjRoot K x (algebraMap K S r) holds exactly when x equals algebraMap K S r.

Русский

Для элемента r IsConjRoot K x (algebraMap K S r) истинно тогда и только тогда, когда x равно algebraMap K S r.

LaTeX

$$$IsConjRoot K x (algebraMap K S r) \iff x = algebraMap K S r$$$

Lean4

/-- An element `x` is a conjugate root of some element `algebraMap R S r` in the image of the base ring
if and only if `x = algebraMap R S r`.
-/
@[simp]
theorem isConjRoot_iff_eq_algebraMap {r : K} {x : S} : IsConjRoot K (algebraMap K S r) x ↔ x = algebraMap K S r :=
  isConjRoot_iff_eq_algebraMap_of_injective (algebraMap K S).injective

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