algebraicIndependent_adjoin_iff — Mathlib

English

For x ∈ S, AlgebraicIndependent (adjoin F s) x is equivalent to AlgebraicIndependent (Algebra.adjoin F s) x; i.e., algebraic independence is preserved when passing from adjoin to Algebra.adjoin.

Русский

Для x ∈ S AlgebraicIndependent (adjoin F s) x эквивалентно AlgebraicIndependent (Algebra.adjoin F s) x; алгебраическая независимость сохраняется при переходе от adjoin к Algebra.adjoin.

LaTeX

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

Lean4

theorem algebraicIndependent_adjoin_iff {x : ι → S} :
    AlgebraicIndependent (adjoin F s) x ↔ AlgebraicIndependent (Algebra.adjoin F s) x :=
  (Algebra.IsAlgebraic.algebraicIndependent_iff ..).symm

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