English
If R has no zero divisors, and s is nonempty, then IsAlgebraic of adjoin R s is equivalent to IsAlgebraic of all elements of s.
Русский
Если R без делителей нуля и s непусто, то IsAlgebraic для adjoin R s эквивалентно IsAlgebraic для каждого элемента s.
LaTeX
$$$[NoZeroDivisors R] \\Rightarrow (s.Nonempty \\Rightarrow ((\\operatorname{adjoin}_R s).IsAlgebraic \\iff \\forall x \\in s, IsAlgebraic_R x))$$$
Lean4
/-- In an algebra generated by a single algebraic element over a domain `R`, every element is
algebraic. This may fail when `R` is not a domain: see https://mathoverflow.net/a/132192/ for
an example. -/
theorem isAlgebraic_adjoin_singleton_iff [NoZeroDivisors R] {s : S} : (adjoin R { s }).IsAlgebraic ↔ IsAlgebraic R s :=
(isAlgebraic_adjoin_of_nonempty <| Set.singleton_nonempty s).trans forall_eq
