isAlgebraic_adjoin_iff_bot — Mathlib

English

AlgebraicIsR (adjoin F s) is equivalent to AlgebraicIsR (Algebra.adjoin F s): the algebraicity relative to R of the adjoin generated by F and s does not depend on whether we view the subalgebra as adjoin or Algebra.adjoin.

Русский

Алгебраичность над R для порождаемого адъёном F s не зависит от того, рассматриваем ли мы подалгебру как adjoin или как Algebra.adjoin.

LaTeX

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

Lean4

theorem isAlgebraic_adjoin_iff_bot : Algebra.IsAlgebraic R (adjoin F s) ↔ Algebra.IsAlgebraic R (Algebra.adjoin F s) :=
  IsAlgebraic.isAlgebraic_iff_bot ..

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