eq_algebraMap — Mathlib

English

If x is a conjugate root of algebraMap K S r over K, then x equals algebraMap K S r.

Русский

Если x - сопряжённый корень algebraMap K S r над K, то x равно algebraMap K S r.

LaTeX

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

Lean4

/-- If `x` is a conjugate root of some element `algebraMap R S r` in the image of the base ring, then
`x = algebraMap R S r`.
-/
theorem eq_algebraMap {r : K} {x : S} (h : IsConjRoot K (algebraMap K S r) x) : x = algebraMap K S r :=
  eq_algebraMap_of_injective h (algebraMap K S).injective

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