English
For a nontrivial R, IsTranscendenceBasis R x is equivalent to IsAlgebraic of adjoin over R of range x together with AlgebraicIndependent R x.
Русский
Для непростой R, IsTranscendenceBasis R x эквивалентно тому, что x алгебраически независим над R и adjoin_R(range x) является алгебраически над A.
LaTeX
$$$ IsTranscendenceBasis R x \iff (AlgebraicIndependent R x \\land Algebra.IsAlgebraic (adjoin R (range x)) A)$$$
Lean4
theorem isAlgebraic [Nontrivial R] (hx : IsTranscendenceBasis R x) : Algebra.IsAlgebraic (adjoin R (range x)) A :=
by
constructor
intro a
rw [← not_iff_comm.1 (hx.1.option_iff_transcendental _).symm]
intro ai
have h₁ : range x ⊆ range fun o : Option ι => o.elim a x :=
by
rintro x ⟨y, rfl⟩
exact ⟨some y, rfl⟩
have h₂ : range x ≠ range fun o : Option ι => o.elim a x :=
by
intro h
have : a ∈ range x := by
rw [h]
exact ⟨none, rfl⟩
rcases this with ⟨b, rfl⟩
have : some b = none := ai.injective rfl
simpa
exact h₂ (hx.2 (Set.range fun o : Option ι => o.elim a x) ((algebraicIndependent_subtype_range ai.injective).2 ai) h₁)
