English
A family x is a transcendence basis over R in A if it is algebraically independent over R and maximal with respect to this property in A.
Русский
Семейство x является базисом трансцендентности над R в A, если оно алгебраически независимо над R и максимально по этой характеристике в A.
LaTeX
$$$\\text{IsTranscendenceBasis } x := \\text{AlgebraicIndependent } R\\, x \\wedge \\forall s, \\text{AlgebraicIndepOn } R\\ id\\, s \\wedge (\\mathrm{range}\,x \\subseteq s) \\rightarrow \\mathrm{range}\,x = s$$$
Lean4
/-- A family is a transcendence basis if it is a maximal algebraically independent subset. -/
@[stacks 030E "(4)"]
def IsTranscendenceBasis (x : ι → A) : Prop :=
AlgebraicIndependent R x ∧ ∀ (s : Set A) (_ : AlgebraicIndepOn R id s) (_ : range x ⊆ s), range x = s
