isAlgebraic_adjoin_of_nonempty — Mathlib

English

A variant: IsAlgebraic Adjoin equivalence expressed with a consequence on membership.

Русский

Вариант: эквивалентность IsAlgebraic для adjoin выражается через принадлежность членов.

LaTeX

$$$\\forall s, IsAlgebraic(\\operatorname{adjoin}_R s) \\iff \\forall x \\; (x \\in s) \\Rightarrow IsAlgebraic_R x$$$

Lean4

theorem isAlgebraic_adjoin_of_nonempty [NoZeroDivisors R] {s : Set S} (hs : s.Nonempty) :
    (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x :=
  ⟨fun h x hx ↦ h _ (subset_adjoin hx), fun h ↦
    have ⟨x, hx⟩ := hs
    have := (isDomain_iff_noZeroDivisors_and_nontrivial _).mpr ⟨‹_›, (h x hx).nontrivial⟩
    isAlgebraic_adjoin_iff.mpr h⟩

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