isAlgebraic_adjoin_iff_top — Mathlib

English

For intermediate fields and subalgebras, the algebraicity of elements with respect to adjoin F s and with respect to Algebra.adjoin F s are equivalent when considered as subalgebras inside S.

Русский

Для промежуточных полей и подалгебр алгебрность элементов относительно adjoin F s и Algebra.adjoin F s эквивалентна, если рассматривать их как подалгебры внутри S.

LaTeX

$$$\\\\mathrm{IsAlgebraic}(\\\\operatorname{adjoin}_F s) S \\\\iff \\\\mathrm{IsAlgebraic}(\\\\operatorname{Algebra.adjoin}_F s) S$$$

Lean4

theorem isAlgebraic_adjoin_iff_top : Algebra.IsAlgebraic (adjoin F s) S ↔ Algebra.IsAlgebraic (Algebra.adjoin F s) S :=
  (IsAlgebraic.isAlgebraic_iff_top ..).symm

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