nonempty_iff_transcendental — Mathlib

English

A transcendence basis over R is nonempty if and only if A is transcendental over R.

Русский

Базис трансцендентности над R непуст тогда и только тогда A является трансцендентальным над R.

LaTeX

$$$ Nonempty ι \iff Algebra.Transcendental R A$$$

Lean4

/-- If `x` is a transcendence basis of `A/R`, then it is not empty if and only if
`A/R` is transcendental. -/
theorem nonempty_iff_transcendental [Nontrivial R] (hx : IsTranscendenceBasis R x) :
    Nonempty ι ↔ Algebra.Transcendental R A := by
  rw [← not_isEmpty_iff, Algebra.transcendental_iff_not_isAlgebraic, hx.isEmpty_iff_isAlgebraic]

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