English
If a conjugate root of a polynomial with value 0 exists and the base map is injective, then it must be 0.
Русский
Если сопряжённый корень константы 0 существует и отображение основания инъективно, то он должен равняться 0.
LaTeX
$$$IsConjRoot\ R\ 0\ x \Rightarrow (algebraMap\ R\ S)\ injective \Rightarrow x = 0$$$
Lean4
/-- A variant of `IsConjRoot.eq_zero`, only assuming `Nontrivial R`,
`NoZeroSMulDivisors R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. If `x` is a
conjugate root of `0`, then `x = 0`.
-/
theorem eq_zero_of_injective [Nontrivial R] [NoZeroSMulDivisors R S] {x : S} (h : IsConjRoot R 0 x)
(hf : Function.Injective (algebraMap R S)) : x = 0 :=
(algebraMap R S).map_zero ▸ (eq_algebraMap_of_injective ((algebraMap R S).map_zero ▸ h) hf)
