isEmpty_iff_isAlgebraic — Mathlib

English

For a transcendence basis x over R, the index type ι is empty if and only if A is algebraic over R.

Русский

Для базиса трансцендентности x над R множество индексов пусто тогда и только тогда A является алгебраическим над R.

LaTeX

$$$ IsEmpty ι \iff Algebra.IsAlgebraic R A$$$

Lean4

/-- If `x` is a transcendence basis of `A/R`, then it is empty if and only if
`A/R` is algebraic. -/
theorem isEmpty_iff_isAlgebraic [Nontrivial R] (hx : IsTranscendenceBasis R x) : IsEmpty ι ↔ Algebra.IsAlgebraic R A :=
  by
  refine ⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩
  have := hx.isAlgebraic
  rw [Set.range_eq_empty x, adjoin_empty] at this
  exact algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left R A

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