algebraicIndependent_iff_transcendental

English

The one-element family is algebraically independent if and only if its element is transcendental.

Русский

Единственный элемент семейства алгебраически независим тогда, когда этот элемент трансцендентен.

LaTeX

$$$\forall {x} : A,\ AlgebraicIndependent R ![x] \iff Transcendental R x$$$

Lean4

/-- The one-element family `![x]` is algebraically independent if and only if
`x` is transcendental. -/
theorem algebraicIndependent_iff_transcendental {x : A} : AlgebraicIndependent R ![x] ↔ Transcendental R x := by simp

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