transcendental_adjoin_iff — Mathlib

English

For x ∈ S, Transcendental (adjoin F s) x is equivalent to Transcendental (Algebra.adjoin F s) x; i.e., transcendence over the adjoin and over the corresponding algebraic adjoin coincide.

Русский

Для x ∈ S Transcendental(адъойн F s) x эквивалентно Transcendental(Algebra.adjoin F s) x; то есть трансцендентность над adjoin и над соответствующим Algebra.adjoin совпадает.

LaTeX

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

Lean4

theorem transcendental_adjoin_iff {x : S} : Transcendental (adjoin F s) x ↔ Transcendental (Algebra.adjoin F s) x :=
  (IsAlgebraic.transcendental_iff ..).symm

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