isConjRoot_iff_eq_algebraMap' — Mathlib

English

A simp variant of the equivalence: IsConjRoot K x (algebraMap K S r) iff x = algebraMap K S r.

Русский

Упрощённый вариант эквивалентности: IsConjRoot K x (algebraMap K S r) эквивалентно x = algebraMap K S r.

LaTeX

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

Lean4

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

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