algebraicIndependent_of_finite_type

English

If for every finite subset t of ι, the finite evaluation x|t is algebraically independent, then x is algebraically independent.

Русский

Если для каждого конечного подмножества t индексов ι семейство x|t алгебраически независимо, то само x алгебраически независимо.

LaTeX

$$$\forall t \subseteq ι,\ t\text{ finite }\Rightarrow \text{AlgebraicIndependent}_R (\lambda i. x i)\big|_{t}$$$

Lean4

theorem algebraicIndependent_of_finite_type (H : ∀ t : Set ι, t.Finite → AlgebraicIndependent R fun i : t ↦ x i) :
    AlgebraicIndependent R x :=
  (injective_iff_map_eq_zero _).mpr fun p ↦
    algebraicIndependent_comp_subtype.1 (H _ p.vars.finite_toSet) _ p.mem_supported_vars

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