isTranscendenceBasis_adjoin_iff — Mathlib

English

For x ∈ S, IsTranscendenceBasis (adjoin F s) x is equivalent to IsTranscendenceBasis (Algebra.adjoin F s) x; the transcendence basis property does not depend on the specific ambient adjoin construction.

Русский

Для x ∈ S свойство IsTranscendenceBasis(adjoin F s) x эквивалентно IsTranscendenceBasis(Algebra.adjoin F s) x; база трансцендентности не зависит от конкретной конструкции adjoin.

LaTeX

$$$\\\\mathrm{IsTranscendenceBasis}(\\\\operatorname{adjoin}_F s) x \\\\iff \\\\mathrm{IsTranscendenceBasis}(\\\\operatorname{Algebra.adjoin}_F s) x$$$

Lean4

theorem isTranscendenceBasis_adjoin_iff {x : ι → S} :
    IsTranscendenceBasis (adjoin F s) x ↔ IsTranscendenceBasis (Algebra.adjoin F s) x :=
  (Algebra.IsAlgebraic.isTranscendenceBasis_iff ..).symm

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