isConjRoot_zero_iff_eq_zero_of_injective

English

Not belonging to the base subalgebra is equivalent to the existence of a different conjugate root over the base field.

Русский

Не принадлежность базовому подалгебро эквивалентна существованию другого сопряжённого корня над базовым полем.

LaTeX

$$$x \notin (\perp) \iff \exists y:\, y \neq x \land IsConjRoot K x y$$$

Lean4

/-- A variant of `IsConjRoot.iff_eq_zero`, only assuming `Nontrivial R`,
`NoZeroSMulDivisors R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. `x` is a
conjugate root of `0` if and only if `x = 0`.
-/
theorem isConjRoot_zero_iff_eq_zero_of_injective [Nontrivial R] {x : S} [NoZeroSMulDivisors R S]
    (hf : Function.Injective (algebraMap R S)) : IsConjRoot R 0 x ↔ x = 0 :=
  ⟨fun h => eq_zero_of_injective h hf, fun h => h.symm ▸ rfl⟩

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