isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic

English

A transcendence basis x is characterized by being algebraically independent over R and by adjoin_R(range x) being algebraic over A.

Русский

Базис трансцендентности x определяется как алгебраически независимый над R набор, для которого adjoin_R(range x) алгебраично над A.

LaTeX

$$$ IsTranscendenceBasis R x \iff (AlgebraicIndependent R x \land Algebra.IsAlgebraic (adjoin R (range x)) A)$$$

Lean4

theorem isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic [Nontrivial R] :
    IsTranscendenceBasis R x ↔ AlgebraicIndependent R x ∧ Algebra.IsAlgebraic (adjoin R (range x)) A :=
  ⟨fun h ↦ ⟨h.1, h.1.isTranscendenceBasis_iff_isAlgebraic.mp h⟩, fun ⟨ind, alg⟩ ↦
    ind.isTranscendenceBasis_iff_isAlgebraic.mpr alg⟩

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