isTranscendenceBasis_iff — Mathlib

English

Let x be a family of elements of A indexed by ι, and suppose R ⟶ S is an integral extension of commutative rings (S is integral over R). Then x forms a transcendence basis over R if and only if it forms a transcendence basis over S.

Русский

Пусть x обозначает семейство элементов A, индексируемое по ι, и пусть S является интегральным расширением над R (S интегрально над R). Тогда x образует базу трансцендентности над R тогда и только тогда, когда она образует базу трансцендентности над S.

LaTeX

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

Lean4

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

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