isTranscendenceBasis_iff — Mathlib

English

If S is algebraic over R, then AlgebraicIndependent R x is equivalent to AlgebraicIndependent S x; this reflects invariance of algebraic independence under algebraic base change.

Русский

Если S является алгебраическим над R, то AlgebraicIndependent R x эквивалентно AlgebraicIndependent S x; это отражает инвариантность алгебраической независимости при алгебраическом базисном изменении.

LaTeX

$$$\\\\mathrm{AlgebraicIndependent}(R,x) \\\\iff \\\\mathrm{AlgebraicIndependent}(S,x)$$$

Lean4

protected theorem isTranscendenceBasis_iff [Algebra.IsAlgebraic R S] :
    IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x := by
  simp_rw [IsTranscendenceBasis, IsAlgebraic.algebraicIndependent_iff R S]

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