English
Under suitable hypotheses, IsConjRoot R (algebraMap R S r) x is equivalent to x = algebraMap R S r.
Русский
При подходящих гипотезах IsConjRoot R (algebraMap R S r) x эквивалентно x = algebraMap R S r.
LaTeX
$$$IsConjRoot R (algebraMap R S r) x \iff x = algebraMap R S r$ (with injectivity).$$
Lean4
/-- A variant of `IsConjRoot.eq_of_isConjRoot_algebraMap`, only assuming `Nontrivial R`,
`NoZeroSMulDivisors R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. 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 isConjRoot_iff_eq_algebraMap_of_injective [Nontrivial R] [NoZeroSMulDivisors R S] {r : R} {x : S}
(hf : Function.Injective (algebraMap R S)) : IsConjRoot R (algebraMap R S r) x ↔ x = algebraMap R S r :=
⟨fun h => eq_algebraMap_of_injective h hf, fun h => h.symm ▸ rfl⟩
