algebraicIndependent_singleton_iff

English

If ι is a singleton, then AlgebraicIndependent R x iff Transcendental R (x at the unique element).

Русский

Если множество индексов единично, то AlgebraicIndependent R x эквивалентно Transcendental R (x на единственном индексе).

LaTeX

$$$\forall \{\iota\} (i:\iota),\ AlgebraicIndependent R x \leftrightarrow Transcendental R (x i)$$$

Lean4

theorem algebraicIndependent_singleton_iff [Subsingleton ι] (i : ι) :
    AlgebraicIndependent R x ↔ Transcendental R (x i) :=
  letI := uniqueOfSubsingleton i
  algebraicIndependent_unique_type_iff

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