English
A family is algebraically independent iff its restriction to a subset is independent and the rest is controlled by an independence-on-adjoin structure.
Русский
Семейство является алгебраически независимым тогда и только тогда, когда его ограничение на подмножество независимо и остальное управляется через стуктуру AlgebraIndepOn над адъойнтом.
LaTeX
$$$\forall {ι} {x : ι \to A}, AlgebraicIndependent R x \iff AlgebraicIndependent R (fun i => x i) ∧ AlgebraicIndepOn (adjoin R (x '' ι)) x (Set.univ \setminus ι)$$
Lean4
/-- Variant of `algebraicIndependent_of_finite` using `Transcendental`. -/
theorem algebraicIndependent_of_finite' (s : Set A) (hinj : Injective (algebraMap R A))
(H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R ((↑) : t → A) → ∀ a ∈ s, a ∉ t → Transcendental (adjoin R t) a) :
AlgebraicIndependent R ((↑) : s → A) :=
algebraicIndependent_of_finite_type' hinj fun t hfin h i hi ↦
H _ (by rintro _ ⟨x, _, rfl⟩; exact x.2) (hfin.image _) h.image _ i.2 (mt Subtype.val_injective.mem_set_image.mp hi)
