English
If y is a conjugate root of algebraMap R S r in S and the base map algebraMap R S is injective, then y equals algebraMap R S r.
Русский
Если y является сопряжённым корнем algebraMap R S r в S и отображение базиса образно инъективно, то y равно algebraMap R S r.
LaTeX
$$$IsConjRoot\ R\ (algebraMap\ R\ S\ r)\ x \Rightarrow (algebraMap\ R\ S)\;\text{injective} \Rightarrow x = algebraMap\ R\ S\ r$$$
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 eq_algebraMap_of_injective [Nontrivial R] [NoZeroSMulDivisors R S] {r : R} {x : S}
(h : IsConjRoot R (algebraMap R S r) x) (hf : Function.Injective (algebraMap R S)) : x = algebraMap R S r :=
by
rw [IsConjRoot, minpoly.eq_X_sub_C_of_algebraMap_inj _ hf] at h
have : x ∈ (X - C r).aroots S := by
rw [mem_aroots]
simp [X_sub_C_ne_zero, h ▸ minpoly.aeval R x]
simpa [aroots_X_sub_C] using this
